Verilog Translator

It is a common case for expressions in Verilog designs to have operands that become wrong via transforming to SMT\SMV format. Here are some examples.

1. In vcegar-tests/mpeg/mpeg_1.v:

reg [15:0] NumBytes;
wire [3:0] timeStampBytes;
...
NumBytes = NumBytes - timeStampBytes;

Operands of "-" have different data types, so SMT solver reports an error.

2. In verilog2smv-vis-tests/Vsa16/vsa16a.v:

output [15:0] ALUOutput;
reg [11:0]      NPC;
wire [15:0]      Imm = {{8{immFld[8]}},immFld[7:0]};
ALUOutput <= {4'd0,NPC} + {Imm,1'b0};

This expression produces the following error in nuXmv model checker:

TYPE ERROR file vsa16a.smv: line 593 : illegal operand types of "+" : unsigned word[16] and unsigned word[17]

3. In twoFifo1.v:

parameter        LOGLENGTH = 2;
...
reg [LOGLENGTH-1:0]    writehead;
...
for (i = 0; i <= LENGTH-1; i = i + 1) begin
if (((writehead < writetail) && (i >= writehead) &&
         (i < writetail)) ||
            ((writehead > writetail) && ((i >= writehead) ||
                     (i < writetail)))) begin
        if ((readempty == 0) &&
        (readfifo[readhead] == writefifo[i])) begin
        match <= 1;
        storeaddr <= readhead;
        end
    end

The unrolled "for" loop produces the error in nuXmv model checker (probably the i counter value has 32-bit vector type):

TYPE ERROR file twoFifo1.smv: line 762 : illegal operand types of "<" : unsigned word[32] and unsigned word[2]

4. In verilog2smv-vis-tests/Ibuf/ibuf.v:

    input [0:2]     flush;
    output [0:1] load0;
    output [0:2] issue0;
    output [0:2] issue1;
    output [0:2] valid;
...
wire nv0 = ~flush[0] & (valid[0] & ~(issue0[0] | issue1[0]) | load0);

This expression produces the following error in nuXmv model checker:

TYPE ERROR file ibuf.smv: line 164 : illegal operand types of "|" : unsigned word[1] and unsigned word[2]

5. In verilog2smv-vis-tests/BufAl/bufferAlloc.v:

    output              nack;
    reg [4:0]          count;
    reg              alloc, free;
...
count = count + (alloc & ~nack) - (free & busy[free_addr]);

This expression produces the following error in nuXmv model checker:

TYPE ERROR file bufferAlloc.smv: line 964 : illegal operand types of "+" : unsigned word[5] and unsigned word[1]