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.