Synopsys Formality help!

[heartfree]

Hello everybody,
I met with a problem about formality. Here is description:

reg dout_reg;
reg [41:0] scan_sig;
reg [5:0] shift_count;
always @ (negedge resetn or posedge clk)
begin
if.................
else
dout_reg <= scan_sig[shift_count]

end
In RTL design, shift_count is guaranted in the range of 0~41. But when I run rtl vs. gate formal verification, the tool reports dout_reg is a failing point.
I analyzed the failing pattern. It seemed that formality regard the scan_sig as "x" when shift_count is larger than 41.
How to avoid this issue?
thanks

 

[sree205]

From what i could understand, dout_reg is a single bit register and you are passing the value of any bit position from 0 to 41 onto the dout_reg.

So, naturally, if the bit position exceeds 41, formality will show an error because bit position exceeding 41 doesn't exist.

Work around will be to have an if,else statement in your constraints to ensure that only values till 41 are used and tie the rest to a constant.

 

[avimit]

Unless you protect your shift_count i.e unless you make sure that shift_count does not exceed 41, your RTL is also not 100% correct. So, put s'thing in your RTL like
if(shift_count >41) then
shift_count = 0
end if;
Now if you run formality, it shouldn't fail.
Hope it helps,
Kr,
Avi
http://www.vlsiip.com