EVENT-BASED VERIFICATION OF SYNCHRONOUS, GLOBALLY CONTROLLED, LOGIC DESIGNS AGAINST SIGNAL FLOW-GRAPHS

We address the problem of automatically verifying large digital design s at the logic level, against high-level specifications. We present a technique which allows for the verification of a:specific class of sys tems, namely systems with synchronous globally timed control. To a fir st 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 F low Graph (SFG) specification, or a specification in an applicative la nguage such as SILAGE. In this paper, a method is presented for verify ing the implementation against an intermediate SFG, which is an expans ion of the original specification in such a way that all the operation s correspond to Register Transfers (RT's) in the implementation. In th is 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 indi ces and computing addresses of memory locations. SFG's can be viewed a s maximally parallel synchronous machines. Both the implementation and the specification are then Finite State Machines, having string funct ions (input/output mappings) associated with them. Correctness is take n to mean that a certain relation (the beta-relation) holds between th ese string functions. This relation extends beyond strict input/output equivalence, and provides room for various behavioral transformations . We present sufficient conditions for the validity of the beta-relati on between the implementation and the expanded SFG. These conditions c an be verified automatically and efficiently. They consist of the comb inational correctness of data path hardware, and the validity of a num ber of past-tense Computation Tree Logic (CTL) formulae expressing con straints on control events. The latter can be verified using Finite St ate Machine (FSM) traversal algorithms. In this way, the verification of the composite machine is reduced to the separate verification of th e data path and the controller. It remains to be shown, after applicat ion of our verification procedure, that the expanded SFG is in beta-re lation with the original SPG. Experimental results are presented.