Event-based verification of synchronous, globally controlled, logic designs against signal flow graphs

We address the problem of automatically verifying large digital designs at the logic level, against high-level specifications. We present a technique which allows for the verification of a specific class of systems, namely systems with synchronous globally timed control. To a first approximation, these are systems where a single controller directs the data through the data path and decides (globally) when to move the data. We address the verification of these systems against a Signal Flow Graph (SFG) specification, or a specification in an applicative language such as SILAGE. In this paper, a method is presented for verifying the implementation against an intermediate SFG, which is an expansion of the original specification in such a way that all the operations correspond to Register Transfers (RT´s) in the implementation. In this SFG, complex arithmetic operations such as multiplications may have been decomposed into simpler ones, such as shifts and additions, and new operations may have been introduced for maintaining iteration indices and computing addresses of memory locations. SFG´s can be viewed as maximally parallel synchronous machines. Both the implementation and the specification are then Finite State Machines, having string functions (input/output mappings) associated with them. Correctness is taken to mean that a certain relation (the β-relation) holds between these string functions