Illustration of the SFG-tracing multi-level behavioral verification methodology, by the correctness proof of a high to low level synthesis application in Cathedral-II

The SFG-tracing methodology addresses the automatic verification of digital synchronous circuit implementations as specified at the algorithmic level as signal- (SFG) or data flow graphs. The SFG-tracing methodology is a multi-level design verification paradigm that aims at bridging the gap between higher level specifications down to lower level implementations up to the transistor switch level. The concepts of the SFG-tracing methodology are illustrated by the automatic verification of a transistor level implementation of a small chip generated from its high level specification by the Cathedral-II silicon compiler. This application, although simple, includes a datapath, register files, a multi-branch micro coded controller, and additional circuitry as necessary for design for testability measures. This application illustrates the SFG-tracing verification methodology as applied to one member of a partitioned SFG behavioral specification. Experimental results on more complex, completely verified designs of 32000 transistors demonstrate the feasibility of the approach