Contents
Hardware Verification using Software Analyzers
Description
Program analysis is a highly active area of research, and the capacity and precision of software analyzers is improving rapidly. We investigate the application of modern software verification tools for formal property checking of hardware given in traditional Verilog at register-transfer level. To this end, we translate the word-level RTL Verilog into an equivalent word-level ANSI-C program using synthesis semantics. The property of interest is instrumented into the C program as an assertion. We subsequently apply three different software verification techniques, which are bounded model checking, path-based symbolic simulation and abstract interpretation, and compare their performance to conventional methods for property verification of hardware designs at netlist and RT-level. Our experimental results indicate that speedups of more than an order of magnitude are possible, enabling the verification of system-level models of hardware IPs. To the best of our knowledge, this is the first attempt to perform system-level property verification of hardware IPs using software verifiers.
Tool Flow
v2c tool translates a synthesizable behavioral Verilog
into a structurally identical ANSI-C code based on synthesis semantics. Different tool interpret
verilog differently. Industry standard tool like Cadence verilog XL are based on scheduling of
events. Synthesizers and cycle simulators are based on less detailed synchronous next-state
semantics. v2c is a source to source translator
based on synthesis semantics and not on simulation semantics or event-queue semantics.
The translator is able to handle synthesizable subset of Verilog.
However, there are various behavioral constructs in Verilog which are non-trivially mapped
to an equivalent C code using a combination of ANSI-C constructs. v2c
ignores the non-synthesizable constructs during the translation process. The tool
reports an error if the input verilog file contains parsing errors.
Contact Rajdeep Mukherjee
with questions about v2c 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 becnhmark collection suite. The
tarball contains both datapath and control-path intensive benchmarks. Each
folder contains safe, unsafe version of the design, properties and run scripts.
Working Example using v2c Translator
The following example illustrates Verilog to ANSI-C translation usingv2c translator tool. This example contains both sequential
and combinational elements, blocking and non-blocking statements.
Verilog to ANSI-C Translation
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 }
Clock-accurate Model Generation
The following example illustrates generation of clock accurate C model from Verilog. Verilog has three kinds of assignments, namely, blocking, non-blocking and continuous assignments.Clock Accurate Translation Example
Verilog ANSI-C
--------------------------- -------------------------------
module M1(Din, CLK, Dout); struct s_M1 {
input Din, CLK; unsigned int q1,q2;
output Dout; } sM1;
reg q1,q2;
wire t; _Bool M1(_Bool CLK, _Bool Din,
assign Dout = q1; _Bool *Dout) {
always @(posedge CLK) _Bool tmp0,tmp1;
q1 <= Din; tmp0 = Din;
if(q1) if(sM1.q1)
q2 <= q1; tmp1 = sM1.q1;
endmodule // update the actual values
sM1.q1 = tmp0;
sM1.q2 = tmp1;
*Dout = sM1.q1;
}
Capturing Module Dependency
Module Dependency Example
Verilog ANSI-C
--------------------------- -------------------------------
module foo(c,a,z,y); #include
input c; struct state_elements_foo{
input [31:0] a; unsigned int y;
output [31:0] z; };
reg [31:0] y; struct state_elements_foo sfoo;
output [31:0] y; void foo_out(_Bool c,unsigned int a,
unsigned int *z, unsigned int *y){
assign z[0] = c; *z=(*z & 0xfffffffe)
| (c & 0x1);
assign z[31:1] = a[30:0]; *z=(*z & 0x00000001)
| ((a & 0x7fffffff)<<1);
}
always@(posedge clk)
y <= z; void foo_ns(_Bool,unsigned int a,
assert property1: ((a == z)); unsigned int *z, unsigned int *y){
endmodule unsigned int tmp0;
tmp0 = *z;
module top(); sfoo.y = tmp0;
wire [31:0] loopback; *y = tmp0;
wire [31:0] y; }
foo f(.c(1),.a(loopback), void main() {
.z(loopback),.y()); unsigned int y, loopback;
endmodule for(i=1;i<33;i++)
// The module in Verilog foo_out(1, loopback, &loopback, &y);
//contains dependency which foo_ns(1, loopback, &loopback, &y);
// feeds each other assert(loopback == 0xffffffff);}
Synthesis Semantics
Translation using Synthesis Semantics
Verilog ANSI-C
--------------------------- -------------------------------
module foo(c,a,z,y); struct module_top {
input c; _u32 loopback;
input [31:0] a; _u32 y;
output [31:0] z; _Bool data;
reg [31:0] y; struct module_foo f;
output [31:0] y; };
extern struct module_top top;
assign z[0] = c; void main() {
assign z[31:1] = a[30:0]; __CPROVER_assume(top.f.z ==
(top.f.z & 0xfffffffe)
always@(posedge clk) | (top.f.c & 0x1));
y <= z; __CPROVER_assume(top.f.z ==
(top.f.z & 0x00000001)
| ((top.f.a & 0x7fffffff) << 1));
endmodule __CPROVER_assume(top.f.c==top.data);
module top(); __CPROVER_assume(top.f.a==top.loopback);
wire [31:0] loopback; __CPROVER_assume(top.f.z==top.loopback);
wire [31:0] y; __CPROVER_assume(top.f.y==top.f.z);
wire data; } //end main
foo f(.c(data),.
a(loopback),.z(loopback),.y());
endmodule
Bit-accurate Model Generation
The following example illustrates generation of bit accurate C model from Verilog usingv2c tool. Verilog supports of extraction operators,
concatenation operator and bitwise operators which are not avaiable in C.
The following code snippet shows some examples of bit-accurate translations.
Bit accurate C model
Verilog ANSI-C
--------------------- ----------------------------------
reg [7:0] in,out; unsigned char in, out;
out[7:5] = in[4:2]; out = out & 0xff1f |
(((in & 0x001c) >> 2) << 5) ;
out[6] = in[4]; out = (out & 0xffbf) |
(((in & 0x0010) >> 4) << 6);
x = { y[5:2], z[6:1] }; x = (((y >> 2) & oxF) << 6)
| ((z >> 1) & 0x3F);
reg [1:0] out; unsigned char out;
if(|out) if(((out >> 1) & 0x1) | (out & 0x1))
Benchmarks
The benchmarks are mainly obtained from opencores. We target datapath and control-path intensive benchmarks in this work. The datapath circuits ranges from DSP domain to various arithmetic cricuits. The control-path intensive benchmarks include USB PHY IP core, Ethernet MAC controller and a simple cache coherence protocol. The cache coherence protocol implementation is obtained from texas97-benchmark suite. Please note that the opencores design often contains non-synthesizable constructs, so we omit these constructs before performing formal verification of these designs using our tool.
Tools Used
We use the following tools in our experiments: v2c, EBMC, HW-CBMC, CBMC, Symex, Astree. 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.
Synthesizable Subset of Verilog
|
Construct Type |
Keywords |
Notes |
Supported |
| ports | input, output, inout | Use inout port only at IO level | ✔ |
| parameters | parameter | Allows more generic design style | ✔ |
| module definition | module | Used to define Verilog module structure | ✔ |
| signals and variables | wire, reg, tri | different signal types, allows vector type | ✔ |
| instantiation | module instance/primitive gate level instances | Used to instantiate one module inside another | ✔ |
| function and tasks | function, task | reduces repeated code, doesnot allow timing | ✔ |
| procedural constructs | always, if, else, case, casex, casez | synthesizable set except initial block | ✔ |
| precedural block | begin, end, named blocks, disable | Allows disabling of named blocks | ✔ |
| Assignment | assign | continuous assignment to wires in combinatorial block | ✔ |
| loops | for, while, forever | looping constructs used in Verilog | ✔ |
| named blocks | disable | Supports disabling of named blocks | ✘ |
Non-synthesizable Subset of Verilog
|
Construct Type |
Notes |
Supported |
| initial | Used only in test benches | ✔ |
| events | Used in test benches for syncing test bench components | ✘ |
| real | Real data type not supported | ✘ |
| force and release | Force and Release data-types not supported | ✘ |
| assign and deassign | assign and deassign on reg type data not supported, but assign supported on wire data type | ✔ |
| fork join | Not supported. Can be simulated using nonblocking assignments | ✘ |
| primitives | only gate level primitives supported | ✔ |
| UDP and Tables | Not supported | ✘ |