Limits of Formality formal verification

[miho]

formality reset

We are trying to use Formality to check if some ECO we performed is correct. Since we want to do only a metal fix, it's a bit of a hack...

In the original netlist, we have DFFs which are reset to 0 by a power-on reset cell. Now we need to change the power-up state (after the power-on reset) of the output of these flip-flops to 1. We did that by connecting the output port to the inverted DFF output and connected the input to an inverted version of the input signal as well.

Functional simulations indicate that this worked fine. The RTL we are comparing with was changed in a clean way, the DFFs are set to 1 at power-on reset.

However, Formality claims that these nets and instances do not match. Is that a limitation of Formality that it cannot recognize that the beahviour from input to output is the same although the state of the DFF is different?

Of course we could change the RTL in the same way we did chaneg the netlict. But that would not allow us to catch any errors in our thinking...

Any suggestions are appreciated. Thanks
Michael

 

[nand_gates]

formal verification limits

I wold like to see ur RTL changes!! Can you give some equivalent example
code here??

 

[miho]

formality reset

Here is the RTL code of the change: the original has been commented out.

always @(posedge wclk or posedge por)
begin
if (por)
begin
r[0] <= 6'b000001; // set bit 0 to ON at power-on reset
// rl[0] <= 0; // the original reset to 0
rl[1] <= 0;
r[2] <= 0;
r[3] <= 0;
end
else
begin
case (byteindex)
4'd0: r[0] <= wdata[5:0];
4'd1: r[1] <= wdata[5:0];

4'd2: r[2] <= wdata[5:0];
4'd3: r[3] <= wdata[5:0];
default: ;
endcase
end
end

Reproducing the netlist is a bit difficult. Hope my message above explains it well enough.

Cheers,
Michael

 

[jackson_peng]

the reset state has change on the output, which fail the verify stage. to avoid this, use the "set dont verify" command to disable check when reset is active low. however, the whole chip reset state will not be check, if it is allowed.

It is recommand to change the RTL after you do the ECO.

 

[miho]

the reset state has change on the output, which fail the verify stage. to avoid this, use the "set dont verify" command to disable check when reset is active low. however, the whole chip reset state will not be check, if it is allowed.

It is recommand to change the RTL after you do the ECO.

Well, we did change the RTL. The RTL simulates fine with the same testbenches as the modified netlist.

However, Formality does not recognize them to be equivalent. That's why I am wondering, if maybe Formality compares register outputs, which are not equivalent in our case. Only the input-output relations are the same between RTL and netlist. Eventually, this is all we care about but it would be reassuring, if Formality would confirm that our changes are correct.