v2c - A Verilog to C Translator Tool
v2c is a Verilog to C translator tool. Given a
Register Transfer Level (RTL) description of a hardware circuit in
Verilog Hardware Description Language
(HDL), v2c is used to automatically translate the Verilog RTL
circuit into a software program which is expressed in C language. The
software program is called software netlist.
Contact Rajdeep Mukherjee
or send an email here with questions
about v2c or feedback.
Download v2c Binary
We distribute pre-compiled static binary of v2c for Linux Systems
|
Download Benchmarks
We distribute several benchmarks in Verilog and ANSI-C for property verification, equivalence checking and simulation.
|
Application of v2c
Description
v2c is primarily used in our hardware property verification
tool flow for translating the hardware circuit given in Verilog RTL into
the software program in C language. The representation of RTL circuit in
a software language allow us to leverage range of software verification
techniques including abstract interpretation and path-wise symbolic execution
which have never been applied to RTL verification.
v2c can also be used for hardware/software co-verification,
equivalence checking and for simulation of the generated C program.
Tool Flow
Working Example using v2c Translator
The following example illustrates Verilog to C translation usingv2c tool. The design contains sequential
and combinatorial logic, procedural blocks, blocking and
non-blocking assignments and multiple module hierarchy. The
code snippet on the left gives the Verilog RTL design and the
code snippet on the right gives the C program.
Verilog 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 {
_Bool ns;
assign Dout = cs; struct s_ff sff;
always @(Din or cs or En) } sen;
begin
if (En) _Bool ff(_Bool CLK, _Bool Din,
ns = Din; _Bool *Dout) {
else _Bool qold;
ns = cs; qold = sen.sff.q;
end sen.sff.q = Din;
ff ff1(ns,CLK,cs); *Dout = qold;
endmodule return;
}
module ff(Din, CLK, Dout); void top(_Bool CLK, _Bool Din,
input Din, CLK; _Bool En, _Bool *Dout) {
output Dout; _Bool cs;
if(En) sen.ns = Din;
reg q; else sen.ns = cs;
assign Dout = q; ff(CLK,sen.ns,&cs);
always @(posedge CLK) *Dout = cs;
q <= Din; }
endmodule int main() {
_Bool CLK,En,Din,Dout;
while(1) {
Din = nondet_bool();
En = nondet_bool();
top(CLK,Din,En,&Dout);
}
return;
}
Handling Multiple Always Blocks
The following example illustrates the handling of multiple always blocks within a module. The procedural blocks contain non-blocking assignments. v2c translator finds the dependencies between different procedural blocks and translates each procedural blocks individually. For example, if every procedural block is driven by same clock event and an update to variable 'x' in procedural block A is read by another procedural block B, then block B must read the old value of the varaible 'x'. If there exist no dependencies between two procedural blocks, then they are translated individually.
Verilog C
----------------------------------- -------------------------
module top(out, enable ,clk, reset); struct state_top {
output [7:0] out; _Bool set;
input enable, clk, reset; unsigned char tout;
reg [7:0] out; _Bool setfound;
reg set, a,b,c; };
reg [7:0] tout; struct state__top stop;
wire found; void top(unsigned char *out,
always @(posedge clk) _Bool enable, _Bool clk,
_Bool reset) {
if (reset) begin _Bool found;
tout <= 8'b0; unsigned char tout_old;
end else if (enable) begin tout_old = stop.out;
tout <= tout + 1; if(reset) stop.tout = 0;
end else if(enable)
stop.tout = tout_old+1;
always @(posedge clk) begin if(stop.out == 2)
stop.set = 1;
if(out==8'h02) else stop.set = 0;
set <= 1'b1;
else if(found == 1)
set <= 1'b0; stop.setfound = 1;
end else
stop.setfound = 0;
always @(posedge clk) begin void main() {
if(found==1'b1) begin unsigned char out;
setfound <= 1'b1; _Bool enable, clk, reset;
end while(1)
else begin top(&out,enable,clk,reset);
setfound <= 1'b0; }
end
end
endmodule
Handling Inter-modular Dependencies
The following example demonstrates the handling of inter-modular dependencies between the continuous assignments and the procedural blocks containing non-blocking assignments.
Verilog 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) {
q1 <= Din; _Bool q1_old, q2_old;
if(q1) q1_old = sM1.q1;q2_old = sM1.q2;
q2 <= q1; sM1.q1 = Din;
endmodule if(sM1.q1)
sM1.q2 = q1_old;
*Dout = sM1.q1;
}
Bit-accurate Software netlist
The following example illustrates generation of bit accurate C program from Verilog usingv2c. Verilog support extraction operators,
concatenation operator, reduction operators which are not available in C.
The following code snippet shows some examples of bit-accurate translation.
Verilog 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);
Combinatorial feedback loop between module
The code snippet below demonstrates handling of combinatorial feedback loop between modules. The output C program shown on the right is generated manually. The global structure of the C program namedtop gives access to all the module elements as well
as instantiates the structure for the submodule foo. The
structure for foo is not shown below but it contains all
the input, output and state-holding elements of foo.
Note that the module hierarchy is lost during translation. However,
the translated program is structurally similar to the synthesized netlist.
We use __CPROVER_assume statements
to assume the generated constraints.
Verilog C Model
--------------------------- -------------------------------
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; };
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
Combinatorial feedback between module preserving module hierarchy
We also demonstrate the translation of the above example where the module hierarchy is retained. This requires determining the stability condition for the combinational exchanges between modules. The combinational part of the design is invoked until the stability condition is reached, which in this case depends on the stability of the values ofa and z. Note that the C program below is
generated manually.
Verilog C
--------------------------- -------------------------------
module foo(c,a,z,y); struct state_elements_foo
input c; {
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,
unsigned int *z, unsigned int *y){
endmodule unsigned int z_old;
z_old = *z;
module top(); sfoo.y = z_old;
wire [31:0] loopback; }
wire [31:0] y;
foo f(.c(1),.a(loopback), int main() {
.z(loopback),.y()); unsigned int y, loopback;
endmodule for(i=1;i<33;i++)
foo_out(1, loopback, &loopback, &y);
foo_ns(1, loopback, &loopback, &y);
}
Limitation of v2c
v2c assumes that the designer has included all the dependent
files in the top level design with the construct `include.
v2c does not support the following design constructs:
Multi-clock designs
Transparent latches
Combinatorial feedback loop
Synthesizable Subset of Verilog
v2c supports the IEEE 1364-2005 Verilog synthesizable standard.
| Construct | 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 | ✔ |
| precedural assignments | blocking, non-blocking | allows assignments to registers in blocking or non-blocking fashion | ✔ |
| 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 | 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 | ✘ |
Co-verification and Equivalence Checking Tool
If you are interested in hardware/software co-verification or C-RTL equivalence checking, please use our tool HW-CBMC.
Bounded Model Checking Tool for Verilog RTL
If you are interested in bounded model checking for Verilog designs, please use our tool EBMC.
Path-based Symbolic Execution Tool
If you are interested in path-based symbolic execution tool for the cycle-accurate C models generated from Verilog or any software (in C) in general, please use our tool VerifOx.