Issues with formal check for RTL vs Netlist

[heartfree]

Formality help!

Hi all,
I met a strange issue when I do formal check for RTL vs. Netlist.

In RTL :
reg [31:0] FIFO [ 3:0];
reg[2:0] Wptr;
always @ (posedge)
if(push)
FIFO[Wptr] = Din[31:0];


FIFO depth is 4, but the Wptr is defined 0~7

I found that FIFO[0] ,FIFO[1],FIFO[2],FIFO[3] are all non-equivalent points.
It seem that Wptr[2] results in these failure.
Does anybody have such experience and know how to solve it?
thanks

 

[jbeniston]

Formality help!

Dunno, but you're missing a clock and should use non-blocking assignments in sequential processes

What is the logic driving Wptr?