Checking consistency of C and Verilog using predicate abstraction and induction

edicate Abstraction and Induction Edmund Clarke Daniel Kroening June 25, 2004 CMU-CS-04-131 School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 It is common practice to write C models of circuits due to the greater simulation efficiency. Once the C program satisfies the requirements, the circuit is designed in a hardware description language (HDL) such as Verilog. It is therefore highly desirable to automatically perform a correspondence check between the C model and a circuit given in HDL. We present an algorithm that checks consistency between an ANSIm and a circuit given in Verilog using Predicate Abstraction. The algorithm exploits the fact that the C program and the circuit share many basic predicates. In to existing tools that perform predicate abstraction, our approach is SAT-based and allows all ANSI-C and Verilog operators in the predicates. We report experimental results on an out-of-order RISC processor. We compare the performance of the new techniq...

• Type: Conference
• Year: 2004
• Where: ICCAD
• Authors: Daniel Kroening, Edmund M. Clarke
• Keywords: Hardware, ICCAD 2004, Motors Collaborative Research, Naval Research Laboratory, Predicate Abstraction