Sequential Equivalence Verification

Problem Definition

When a new device is designed, a "golden model" is often written in a high-level pro­gramming language like ANSI-C, C++, or SystemC. This model is extensively simulated to ensure both correct functionality and performance. Later, a Verilog implementation is cre­ated. 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 equi­valence checker is required.

From IEEE Design & Test of Computers, Volume 18, Issue 4, 2001

Benchmarks

We provide a set of benchmark files that are free of IP concerns in order to enable a meaning­ful 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

Benchmark	Obtained from	Links
adpcm	memcode 07 paper	sc-l sc-h v pic
b01	ITC 99	sc-l sc-h v pic
BCD_uiuc	DAES 08 paper	sc-l sc-h v pic
byte_mixcolum	128/192 AES project	sc-l sc-h v pic
directcontrol	USB1.1 Host and Function Project	sc-l sc-h v pic
fft_flpt	SystemC 2.2 Example	sc-l sc-h v pic
fir_rtl	SystemC 2.2 Example	sc-l sc-h v pic
hostSlaveMux	USB1.1 Host and Function Project	sc-l sc-h v pic
hostSlaveMuxBI	USB1.1 Host and Function Project	sc-l sc-h v pic
ia-32	DAC 06 paper	c sc-h v pic
key_gen	128/192 AES project	sc-l sc-h v pic
mixcolum	128/192 AES project	sc-l sc-h v pic
usbTxWireArbiter	USB1.1 Host and Function Project	sc-l sc-h v pic
wb_master_model	USB1.1 Host and Function Project	sc-l sc-h v pic
word_mixcolum	128/192 AES project	sc-l sc-h v pic
Y86-DT	Digitaltechnik book	sc-l sc-h v pic
bios_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
control_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
dcache_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
exec_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
fetch_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
floating_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
icache_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
mmxu_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
paging_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
pic_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
registerfile_risc_cpu	SystemC 2.2 Example	sc-l sc-h v pic
risc_cpu	SystemC 2.2 Example	sc-l sc-h v

We provide:

• A detailed description of each benchmark
• A tarball with all benchmarks: v2sc_benchmarks_all.tar.gz

Tools

We provide 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 equi­valence checking and co-verification. The benchmark collection above contains scripts to execute hw-cbmc. The binary of hw-cbmc is shipped together with CBMC.

Relevant Publications

• 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.

Patents

• 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