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 #1

Updated by Sergey Smolov over 4 years 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
Actions #2

Updated by Sergey Smolov over 4 years ago

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

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

Actions #3

Updated by Sergey Smolov over 4 years ago

  • Status changed from Resolved to Verified
Actions #4

Updated by Sergey Smolov over 4 years ago

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

Also available in: Atom PDF