Combining Theorem Proving and Model Checking for Certification of Behavioral Synthesis Flows

S. Ray, Y. Chen, F. Xie, and J. Yang

Technical Report TR-08-48, Department of Computer Sciences, University of Texas at Austin, December 2008.


We develop a framework for certifying behavioral synthesis flows. Certification is decomposed into verified and verifying components, which are discharged by theorem proving and model checking respectively. The bridge between these components is provided by a new formal structure, clocked control data flow graph (CCDFG), that serves as the golden circuit model used in this framework. We discuss how CCDFGs facilitate both theorem proving and model checking. The semantics of CCDFGs have been formalized with the ACL2 theorem prover, and the formalization used to certify generic synthesis transformations. Finally, we extend GSTE to model check synthesized netlists with respect to CCDFG specifications.

Relevant files