Computer Science Department
School of Computer Science, Carnegie Mellon University


Checking Consistency of C and Verilog
using Predicate Abstraction and Induction

Edmund Clarke, Daniel Kroening

June 2004

Keywords: Predicate abstraction, Verilog, SAT, equivalence checking

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 ANSI-C program 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 contrast 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 technique to Bounded Model Checking (BMC).

16 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by