Project

General

Profile

Bug #9784

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

Added by Sergey Smolov 4 months ago. Updated 3 months 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

History

#1

Updated by Sergey Smolov 4 months ago

  • Subject changed from mul_fifo.v: wrong Fortress expressions of assignments references to mul_fifo.v: wrong Fortress-based node representation of assignment left-hand side
#2

Updated by Sergey Smolov 4 months ago

  • % Done changed from 0 to 100
  • Assignee changed from Alexander Kamkin to Sergey Smolov
  • Status changed from New to Resolved

The problem was caused by the internal elaborator. An error appeared when top module and it's sub-module (that is produced by loop generate statement) have signals with the same name. To solve this, all the variables of top level module were renamed with "module name" prefix.

Fixed in 5b9be1fd

#3

Updated by Sergey Smolov 3 months ago

  • Status changed from Resolved to Verified
#4

Updated by Sergey Smolov 3 months ago

  • Published in build set to 0.1.2-beta-190909
  • Status changed from Verified to Closed

Also available in: Atom PDF