VerifOx -- A Tool for Path-wise Symbolic Execution

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 embody this technique in our tool, VerifOx. VerifOx is a path-based symbolic execution tool for equivalence checking of C programs. VerifOx supports the C89 and C99 standards. The key feature of VerifOx is symbolic reasoning on the equivalence between floating-point operations. To this end, VerifOx implements a model of the IEEE 754 arithmetic operations such as single- and double-precision addition and subtraction operations, which can be used as reference models. Note that the floating-point reference models in VerifOx are equivalent to the Berkeley SoftFloat library.

VerifOx is implemented in C++. VerifOx is built on top of CPROVER framework. The tool has been successfully used to verify Floating-point unit in ARM GPU against its built-in reference models. VerifOx has also been used for property verification of embedded softwares such as Universal Asynchronous Receiver Transmitter (UART), Ethernet MAC controller, USB PHY IP core and other data and control intensive designs. Some of these benchmarks are available here.

System Requirements

We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
You need a C/C++ compiler, Flex and Bison, and GNU make. The GNU Make needs to be version 3.81 or higher. On Debian-like distributions, do
    apt-get install g++ gcc flex bison make git libz-dev libwww-perl patch libzip-dev
On Red Hat/Fedora or derivates, do
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch

Compiling VerifOx

Step 1: Download VerifOx from http://www.cprover.org/verifox/
Step 2: Check out CBMC source via
            git clone https://github.com/diffblue/cbmc cbmc-git
Step 3: Navigate to VerifOx directory -- cd VerifOx
Step 4: cd src
Step 5: mv config.inc.template config.inc
Step 6: Point the CBMC variable in config.inc file to point to cbmc
            that you downloaded in Step 2. Example: CBMC = /users/rajdeep/cbmc/
Step 7: make
Step 8: cd hasco
Step 9: The executables are :
            -- verifox-pi (partial incremental)
            -- verifox-fi (full incremental)

Using VerifOx

The following command is used to run VerifOx in partial incremental mode with SAT backend.

The following command is used to run VerifOx in partial incremental mode with SMT backend.

The following command is used to run VerifOx in full incremental mode with SAT backend.

Equivalence Checking using HW-CBMC

Description

HW-CBMC is used for C versus Verilog RTL combinational and sequential equivalence checking. HW-CBMC supports IEEE 1364-2005 System Verilog standards and the C89, C99 standards. HW-CBMC maintains two separate flows for hardware and software. The hardware flow uses synthesis to obtain either a bit-level or a word-level netlist from Verilog RTL. The software flow illustrates the translation of the C program into static single assignment (SSA) form. These two flows meet only at the solver. Thus, HW-CBMC generates a monolithic formula from the C and RTL description, which is then checked with SAT/SMT solvers. HW-CBMC provides specific handshake primitives such as next_timeframe() and set_inputs() that direct the tool to set the inputs to the hardware signals and advance the hardware clock, respectively.

Tool Flow

The following command is used to automatically generate the top-level interface from the Verilog files.

The following command is used to run HW-CBMC in bit-level mode.

The following command is used to run HW-CBMC in word-level mode.

Authors: Saurabh Joshi Daniel Kroening Rajdeep Mukherjee

Contact Rajdeep Mukherjee, Saurabh Joshi with questions or feedback.

Equivalence of Verilog and ANSI-C

              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                          }

Example of Trace Partitioning

        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));
} 

        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;}
} 
}
}