Sequential Equivalence Verification
When a new device is designed, a "golden model" is often written in a high-level programming language like ANSI-C, C++, or SystemC. This model is extensively simulated to ensure both correct functionality and performance. Later, a Verilog implementation is created. It is essential to check if the C and Verilog programs are consistent. In general, high-level models are used as specifications in a variety of modeling styles. If the high-level model is not cycle-accurate, or if the set of state-holding elements differs, a sequential equivalence checker is required.
From IEEE Design & Test of Computers, Volume 18, Issue 4, 2001
We provide a set of benchmark files that are free of IP concerns in order to enable a meaningful quantitative comparison of the various techniques. We provide the following types of files:
- sc-l: low-level SystemC, cycle-accurate, identical state
- sc-h: high-level, untimed TLM SystemC
- v: Verilog RTL, usually synthesizable
hw-cbmc, a variant of the
bounded model checker CBMC, to verify combined models
that are extracted from C/C++/SystemC and Verilog. The tool can be used for
equivalence checking and co-verification. The benchmark collection
above contains scripts to execute
hw-cbmc. The binary of
hw-cbmc is shipped together with CBMC.
- Verification of SpecC using Predicate Abstraction
- Formal Verification of SystemC by Automatic Hardware/Software Partitioning
- Checking Consistency of C and Verilog using Predicate Abstraction and Induction
- Hardware Verification using ANSI-C Programs as a Reference
Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
A long version of this paper is availabe as CMU Technical Report.
- Method and system to check correspondence between different representations of a circuit
- Method and system to verify a circuit design by verifying consistency between two different language representations of a circuit design
This research is supported by Intel Research, Haifa, and by the Semiconductor Research Corporation (SRC) under contract no. 2006-TJ-153.