Project

General

Profile

Task #9311

type casting of expression operands

Added by Sergey Smolov over 1 year ago. Updated 6 months ago.

Status:
Closed
Priority:
High
Assignee:
Target version:
Start date:
10/05/2018
Due date:
% Done:

100%

Estimated time:
Detected in build:
master
Published in build:

Description

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]

History

#1

Updated by Sergey Smolov 7 months ago

  • Assignee changed from Alexander Kamkin to Sergey Smolov
#2

Updated by Sergey Smolov 7 months ago

  • Status changed from New to Open
#3

Updated by Sergey Smolov 6 months ago

  • % Done changed from 0 to 100
  • Status changed from Open to Resolved

Done in 290a554b

#4

Updated by Sergey Smolov 6 months ago

  • Status changed from Resolved to Verified
#5

Updated by Sergey Smolov 6 months ago

  • Status changed from Verified to Closed

Also available in: Atom PDF