Sciweavers

Share
DAC
2003
ACM

Behavioral consistency of C and verilog programs using bounded model checking

12 years 2 months ago
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...
Edmund M. Clarke, Daniel Kroening, Karen Yorav
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2003
Where DAC
Authors Edmund M. Clarke, Daniel Kroening, Karen Yorav
Comments (0)
books