[SOLVED] LEC Conformal non-Equivalence Debug

HI

I have some problems about Cadence LEC Conformal after I run the comparison between RTL and Synthesis result. It shows non-equivalence after running a full comparison but I don't know how to solve it since the schematic is too large to debug. I'd like to seek some ideas about what happened to this ?

Here are some part of my Pipeline MIPS code:

assign next_regIfId_ins = ( lw_stall )?regIfId_ins (Branch && equal) || jr || jalr )?32'd0: IN_ReadData;

assign next_regIfId_PC4 = ( lw_stall )?regIfId_PC4 (Branch && equal) || jr || jalr )?32'd0: PCnext;

always @ ( posedge clk or negedge rst_n ) begin
if ( !rst_n )
begin
regIfId_ins <= 32'd0;
regIfId_PC4 <= 32'd0;
end
else
begin
regIfId_ins <= next_regIfId_ins;
regIfId_PC4 <= next_regIfId_PC4;
end
end

However, the LEC Conformal shows non-equivalence comparison for these two signal since they are MUX and NAND respectively. I know that the NAND is flatten result after synthesis. But I have written a high level mux for test and it's correct for LEC Conformal. This confuse me a lot and I have no idea about how to debug this error.

I'd like to seek your help with your experiences. Thanks a lot anyway.
PoLo

read the following commands:

set datapath option
set analyze option
analyze datapath
analyze nonequivalent
analyze retiming
analyze setup

maybe, those will guide you to get right results.

Most typical reason to get mismatches on formal verification is unmapped points, that is, while RTL has sequential elements, the netlist doesn't have corresponding flops/latches due to the synthesis tool having optimized them away.
Look for the unmapped points in the log file, and see if those unmapped points have constant values in RTL. Set constant to those flops if they are constant.

My wild guess is that some bits of IN_ReadData is actually 0 so that those bits in regIfId_ins never toggles(reset value is 0, and the other condition also provides 32'b0) and synthesis tool removed them.

The same is also true for regIfId_PC4. Guessing from the name, is it PC ? If so, unless instructions are byte length(I'm sure MIPS instructions are 32bit wide), a few lower bits(the lowest 2 bits) are NOT in use which makes them fix to 0 ?

To Kaisia: Are you means that key in this command in setup mode in LEC Conformal ?
To lostinxlation: The way you said is meaningful such that I have some "unmapped points" due to this. However, I can make sure the above signal is all used in my application since I treat this as 32 bits signal. In the other words, it's not the unmapped problem. Instead, it's " non-equivalence" problem.

Thanks for all your reply. I have also got suggestion from my institution that he said I might use Formality to check out the equivalence instead of LEC Conformal. I'll try all these method anyway.

I have no ideas about what happen. It seem that there is error in my code such that the synthesis result is non-equivalent because I have written a another simple code for test hierachy and it's true...:sad:

YuLongHuang said:

To lostinxlation: The way you said is meaningful such that I have some "unmapped points" due to this. However, I can make sure the above signal is all used in my application since I treat this as 32 bits signal. In the other words, it's not the unmapped problem. Instead, it's " non-equivalence" problem.

Click to expand...

I think you misunderstand how formal verifications work. The fact that all the bits are being used doesn't mean those bits are always mapped, because mapping is done on the flops/latches upstream of that given logic cone. Whether they are used at the downstream of the logic is irrelevant.
Like you said, you see unmapped point, and that's clearly a sign it's most probably mapping issue causing the mismatches. Think how formal verification works and what would happen if you have unmapped points.

And the 2nd flops in your code, MIPS instructions are always 32 bit wide and any RISC instructions are word aligned for simplicity. It's defined in the MIPS instruction set and you can't change it for your implementation. What it means is bit 0 and 1 of the program counter are always 0. I have designed 32bit and 64bit microprocessors for many years and this is always the case for RISC processors. Trace back the PCnext towards upstream, and I'd think you'll see what i mean.

according to my experience, i encounter those non-equivalences, or aborts just when i didn't set right compare setup condition. the verilog functions are designed correctly.

To lostinxlation:
I don't know whether I realized what you said correctly: Is this means if there are two nets with same functionality even they are both used, the Design Compiler may combine them and hence cause LEC Conformal failure ?

Because I have run the Formality for the same design instead, the final result of Formality shows no error since there is .svf file imported first. In other words, Formality pass but LEC Conformality failed. Does this means that there is something edited by DC in the synthesis process because the compare rule for Formality is exactly mapped ?

Is it means that there is some drawbacks (not error) in my RTL code ? However, to guarantee the synthesis result, does this means that I have to modify my RTL code until the LEC Conformal pass ?

Really appreciate!:grin:
PoLo

// --------------------------------------//
Wow.... How amazing the result after I apply one command for this situation!
I've searched for this solution for long time and just then I find it useful for this.

remodel -seq_constant -repeat -golden
-------------http://www.deepchip.com/items/0465-03.html

I knows that there are 32 DFF which is constant for register0 but I don't care about this since it's well-known. But I don't know why this redundant unmapped fault will cause other comparison failure. This also confused me.

For summary, I solve this non-equivalent problem ( if it's really ... ) but I don't why this happened. So I'll appreciate if you all could give me some ideas.
Q1. The used signal can be midifed by DC ? For example the same functionality ?
Q2. Why the result of Conformal LEC could be different from Formality ?
Q3. To guarantee the synthesis result is coherent with RTL, Conformal LEC is the most important index ?
Q4. Why does the unmapped points will influence other points ? In this case, the other signal such as IN_Addr is correct after I have remodel the constant DFF for LEC Conformal even though it's wrong before.

Thanks for all help!
PoLo

YuLongHuang said:

To lostinxlation:
I don't know whether I realized what you said correctly: Is this means if there are two nets with same functionality even they are both used, the Design Compiler may combine them and hence cause LEC Conformal failure ?

Click to expand...

Just the function of two nets getting combined to the same logic doesn't make formal verif fail, as long as all the keypoints is mapped. What makes it fail is missing mapping of the key points and it happens most often to the removed flops due to redundancy.

Suppose you have this logic,
Since bit 0 of q is always 0, the synthesis tool will generate a netlist like,

Formal verif tool tries to map q[0] and q[1] and it fails to map q[0] because the flop for q[0] doesn't exist in the netlist. This makes the comparison fail on out[0] when formal verif evaluates the case where q[0] is 1.
Formal verif tool cannot see the logic beyond the flops/latches(at least, till recently), so that even though RTL assigns the constant value to q[0], the tool cannot see it when it evaluates the equivalency of the out[1:0] and it assigns whatever value to q[0] when it compares the logic. Obviously, the comparison fails when q[0] gets assigned with 1, where out[0] gets 1 in the golden, and gets 0 in the revised.
That's how the comparison on formal verif fails.

Formality has the different algorithm, especially when you use .svf, everything that was done by synthesis tool is passed down to the formal verif tool. This includes the information about constant nets and deleted flops due to the redundancy, therefore it passed on your netlist/rtls.

Is it means that there is some drawbacks (not error) in my RTL code ? However, to guarantee the synthesis result, does this means that I have to modify my RTL code until the LEC Conformal pass ?

Really appreciate!:grin:
PoLo

Click to expand...

The best thing to do is removing the redundancy in the rtls, but it may not be possible all the time and it takes a lot of effort. When I ran LEC, I always manually checked the mapping and fix them in the LEC script, mostly by setting the constraints to those constant nets.

Q1. The used signal can be midifed by DC ? For example the same functionality ?
Q2. Why the result of Conformal LEC could be different from Formality ?
Q3. To guarantee the synthesis result is coherent with RTL, Conformal LEC is the most important index ?
Q4. Why does the unmapped points will influence other points ? In this case, the other signal such as IN_Addr is correct after I have remodel the constant DFF for LEC Conformal even though it's wrong before.

Click to expand...

Q1: yes DC can do whatever it can do to improve the timing as long as it can maintain the flop to flop functionality.
Q2: Different companies, different algorithm/approach.
Q3: It's just another tool. It works if you know how to handle it. there are many reasons that some companies want to use LEC over Formality and some of the reason is financial/licensing reason.. I used them both till 2 years ago, I perosnally prefer LEC over Formality, but I think formality is more automated.
Q4: Read my comments above.

To lostinxlation:
I really appreciate your help and illrustration. This help me a lot in the sense of verification tool and I've known what is going wrong before.

Thanks!
Best Regards.
PoLo

Mr. lostinxlation! Very good suggestions. We could definitely use these hints in our CAD flows as well.
One additional suggestion to get clean and easy mapping is to maintain intermediate netlists prior to optimization from the synthesis tool. This way, you will be running 2 passes of synthesis
(RTL) <--> (intermediate netlist w/o optimization) <--> final netlist with optimization

This way you have a much more complete and successful completion of your formal verification runs.

Regarding the comment about Formality vs. Conformal. I have become very afraid of Formality. One of our design groups had a dead chip that Formality said was clean. The reason why is because there were optimizations that was too similar between Formality and DC. Conformal-LEC found the problem. Here's the public posting from our design group . .

Conformal finds DC/PhysOpt was missing 40 DFFs that Formality claimed was incorrectly clean