msuen
Newbie
Hi, I am beginner with little experience on Synopsys Formality, and I am having trouble verifying an ECO post-synthesis netlist and manual ECO - post-layout netlist. The problem is described below:
RTL RTL (ECO fix)
| / |
| / |
Synthesis netlist / |
| Formality Equivalent Synthesis netlist (with ECO fix)
| / /
PnR netlist / Formality Not Equivalent
| / /
| / /
Manual ECO (gate level netlist)
I manually edited a gate-level netlist, and is able to verify it equivalency to the new RTL. However, when trying to verify its equivalency to the new synthesized netlist, the equivalency check failed.
My question is, whether Synopsys formality could verify this type of gate level vs gate level netlist check, and if not why is it?
I have provided both the original and new svf file within my script, and I am sure I am using the same version for both design compiler and formailty.
RTL RTL (ECO fix)
| / |
| / |
Synthesis netlist / |
| Formality Equivalent Synthesis netlist (with ECO fix)
| / /
PnR netlist / Formality Not Equivalent
| / /
| / /
Manual ECO (gate level netlist)
I manually edited a gate-level netlist, and is able to verify it equivalency to the new RTL. However, when trying to verify its equivalency to the new synthesized netlist, the equivalency check failed.
My question is, whether Synopsys formality could verify this type of gate level vs gate level netlist check, and if not why is it?
I have provided both the original and new svf file within my script, and I am sure I am using the same version for both design compiler and formailty.