System level verification of video and image processing specifications

TLDR

The paper presents a formal verification method to check loop ordering in high‑level transformed descriptions against their original specifications. The method automatically verifies loop ordering with complexity independent of loop bounds and can handle any practical loop‑nest structure. The approach is effective for speech, image, video processing, telecom, and numerical computing systems, with efficiency demonstrated on several realistic examples.

Abstract

Abstract: A formal verification method is presented to verify the loop ordering of a high level transformed description against its original specification. The verification is done in an automatic way and its complexity is independent on the sizes of the loops bounds. Any practical structure of loop nests can be handled. The method is especially suited for applications in the area of speech, image and video processing, front-end telecom and numerical computing systems which exhibit many loops and complex multi-dimensional signals. The efficiency of the approach is demonstrated on several realistic examples.