Contents
Equivalence Checking using Directed Trace Partitioning
Description
One application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. The partitioning is performed in tandem in both models, exploiting the structure present in the high-level model. The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits.
Tool Flow
Contact Rajdeep Mukherjee with questions or feedback.
Download
The collection of benchmarks in Verilog and in ANSI-C is available for download.
|
Installation
Download the latest tarball of Benchmark suite. Extract its content,
and you can access the Verilog and ANSI-C benchmark collection suite. The
tarball contains both datapath and control-path intensive benchmarks. Each
folder contains the design files and run scripts.
Equivalence of Verilog and ANSI-C
The following example illustrates the equivalence of Verilog and ANSI-C program. This example contains both sequential and combinational elements, blocking and non-blocking statements.Equivalence of Verilog and ANSI-C program
Verilog ANSI-C
------------------------------ ------------------------------
module top(Din,En,CLK,Dout); struct s_ff {
wire cs; reg ns; _Bool q;
input CLK, Din, En; } sff;
output Dout;
struct s_en {
// Combinational Block _Bool ns;
assign Dout = cs; struct s_ff sff;
always @(Din or cs or En) } sen;
begin // Combinational Logic
if (En) void top(_Bool CLK,_Bool Din,
ns = Din; _Bool en, _Bool *Dout) {
else _Bool cs;
ns = cs; if(En) sen.ns = Din;
end else sen.ns = cs;
ff ff1(ns,CLK,cs); ff(CLK,sen.ns,&cs);
endmodule *Dout = cs;
}
// Sequential Block // Sequential Block
module ff(Din, CLK, Dout); _Bool ff(_Bool CLK, _Bool Din,
input Din, CLK; _Bool *Dout) {
output Dout; _Bool tmp0;
reg q; tmp0 = Din;
assign Dout = q; sff.q = tmp0;
always @(posedge CLK) *Dout = sff.q;
q <= Din; return;
endmodule }
Benchmarks
The combinational designs for single precision floating point adder and substractor are developed inhouse. Whereas the single precision and double precision arithmetic circuits for divider and multipler circuit are obtained from softfloat library. Most of the benchmarks for sequential logic are mainly obtained from opencores. We target both datapath and control-path intensive benchmarks in this work. The datapath designs contains arithmetic circuits like single-precision and double-precision floating point adder, subtractor, multiplier and divider circuits. The control-path intensive benchmarks include USB PHY IP core, Ethernet MAC controller and a simple cache coherence protocol. The cache coherence benchmarks was obtained from texas97-benchmark suite Please note that the opencores design often contains non-synthesizable constructs, so we omit these constructs before performing equivalence checking of these designs using our tool.
An Example for Trace Partitioning
The following example illustrates input-based trace partitioning for combinational logic.Input based Case-splitting of Verilog and ANSI-C program
Miter Logic Input-based Partitioning
----------------------- ----------------------------------
void miter(float f, float g){
//setting up the inputs
to hardware FPU //Partition1:
fp_add_sub.f=*(unsigned *)&f; (fp_add_sub.roundingMode==RNE)
fp_add_sub.g=*(unsigned *)&g; && (fp_add_sub.uf_nan)
fp_add_sub.isAdd=1; && (fp_add_sub.ug_nan);
//propagates inputs
of the hardware circuit //Partition2:
set_inputs(); (fp_add_sub.roundingMode==RNE)
//get result from && (fp_add_sub.uf_inf)
hardware circuit && (fp_add_sub.ug_nan);
float Verilog_result=
*(float *)&fp_add_sub.result;
//compute fp-add in Software
with rounding mode RNE
float C_result=add(RNE, f, g);
//compare the outputs
assert(compareFloat
(C_result, Verilog_result));
}
The following example illustrates transaction-based trace partitioning for sequential logic.
Transaction-based partitioning of Verilog and ANSI-C program
Design Transaction-based Partitioning
----------------------- ----------------------------------
#define threshold 15
if(reset) {
mode=0,turn=0;
feedback=0; // Power gated logic partition
} Transaction1: (reset==0) && (env==1)
else { && (mode == STAND_BY) &&
// code fragment for IP (voltage_level == 10);
// Trigger IP if env is set
if(env) { // Normal logic partition
mode = 1; Transaction2: (reset==0) && (env==1)
turn = 0; && (mode == HIBERNATE) &&
// check the voltage level (voltage_level == 20);
if(voltage_level < threshold)
power_gated = 1;
else power_gated = 0;
// check the low-power modes
if(mode == STAND_BY || mode == TURN_OFF) {
// power gated logic.
if(power_gated) {
trans(reset,mode,power_gated, ser_in,&buf_out);
feedback = LOW; // no transmission
}
else { // normal logic
trans(reset,mode,power_gated, ser_in,&buf_out);
feedback = buf_out;}
}
}
}
Tools Used
We used the following tools in our experiments. CBMC is used for C versus C combinational equivalence checking. The tool HW-CBMC is used for C versus Verilog RTL combinational and sequential equivalence checking. The benchmarks and experimental data can be found in the Download section.
Simulation vs Synthesis
In a HDL like Verilog or VHDL not every thing that can be simulated can be synthesized. There is a difference between simulation and synthesis semantics. Simulation semantics are based on sequential execution of the program with some notion of concurrent synchronous processes. Not all such programs can be synthesized. It is not easy to specify the synthesizable subset of an HDL.