Behavioral consistency of C and verilog programs using bounded model checking

We present an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking. Both the circuit and the program are unwound and translated into a formula that represents behavioral consistency. The formula is then checked using a SAT solver. We are able to translate C programs that include side effects, pointers, dynamic memory allocation, and loops with conditions that cannot be evaluated statically. We describe experimental results on various reactive circuits and programs, including a small processor given in Verilog and its Instruction Set Architecture given in ANSI-C. Categories and Subject Descriptors B.5.2 [Hardware]: Register-Transfer-Level Implementation--Design Aids; F.3.1 [Theory of Computation]: Logics and Meanings of Programs--Specifying and Verifying and Reasoning about Programs General Terms Verification Keywords Verilog, ANSI-C, Equivalence Checking ?This research was sponsored by the Semiconductor Rese...

• Type: Conference
• Year: 2003
• Where: DAC
• Authors: Edmund M. Clarke, Daniel Kroening, Karen Yorav
• Keywords: Behavioral Consistency, DAC 2003, Design Automation, Motors Collaborative Research, Naval Research Laboratory