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

v2c binary

Download v2c binary

Download Benchmarks

We distribute several benchmarks in Verilog and ANSI-C for property verification, equivalence checking and simulation.

Property Verification Benchmarks

Verilog RTL and C benchmarks with Safety Assertions

Equivalence Checking and Simulation Benchmarks

Verilog RTL and C benchmarks

Application of v2c


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

Work Flow

Working Example using v2c Translator

The following example illustrates Verilog to C translation using v2c 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; 
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();

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


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 using v2c. 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 named top 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),.

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 of a 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.