Project

General

Profile

Actions

Bug #9784

closed

mul_fifo.v: wrong Fortress-based node representation of assignment left-hand side

Added by Sergey Smolov over 4 years ago. Updated over 4 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Target version:
Start date:
08/01/2019
Due date:
% Done:

100%

Estimated time:
Detected in build:
master
Platform:
Published in build:
0.1.2-beta-190909

Description

Representation that VeriTrans produces on fifo0/mul_fifo.v module contains errors in assignments - Fortress expressions of left-hand side targets are incorrect. For example, one may contain SELECT(x 0), where x is NOT array (map), in the node field of assignment's reference.

In the above Verilog example the situation arises via the following code's processing. The assignment from myfifo.v Verilog file has (SELECT one_fifo.DO_tmp 00000000000000000000000000000000)
Fortress expression in it's left hand side, where one_fifo.DO_tmp has (BIT_VECTOR 8) data type.

mul_fifo.v:

module mul_fifo(
...

//------Parameters declaration:---------
    parameter  FCOUNT_SIZE = 2;
    parameter  DATA_SIZE   = 8;    

//--------------------------------------
wire [(DATA_SIZE-1):0] DO_tmp [((1 << FCOUNT_SIZE)-1):0];
...

generate
    genvar i;
    for (i=0; i!=(1 << FCOUNT_SIZE); i=i+1) begin
        myfifo #(ADDR_SIZE,DATA_SIZE) one_fifo(
        .DO(DO_tmp[i]),
        ...
    end
endgenerate
endmodule

myfifo.v:

`ifndef _MY_FIFO_
`define _MY_FIFO_

`define NAME myfifo

...
module `NAME (
DO,
...);

//------Parameters declaration:---------
    parameter  ADDR_SIZE   = 4;
    parameter  DATA_SIZE   = 8;    
//--------------------------------------

output [(DATA_SIZE-1):0] DO;      // Data Output
...
wire [(DATA_SIZE-1):0] DO_tmp;

always @(posedge CLK) begin
   ...
    DO <= DO_tmp;
   ...
end
...
endmodule
`endif

Actions

Also available in: Atom PDF