Missing DFF in Netlist Causes Unmapped in LEC

[jiwei]

Hi everyone,


I'm currently using LEC to perform RTL-to-netlist equivalence checking, and I've run into an issue.
In my RTL, there is a reg , but after synthesis with Design Compiler, the corresponding DFF doesn't appear in the netlist.
This causes the register to be unmapped during the mapped comparison stage in LEC.

I’ve also tried using the following command, but it didn’t resolve the issue

set undriven signal 0 -both
set flatten model -nodff_to_dlat_feedback -seq_constant -gated_clock -seq_constant_x_to 0 -enable_analyze_hier_compare
remodel -seq_constant -seq_merge -repeat


Has anyone encountered a similar issue or know how to resolve this? Any suggestions would be greatly appreciated. Thanks!

 

[ThisIsNotSam]

If the flop is a constant 0/1, it can be removed by synthesis. If a flip-flop is redundant, it can be removed by synthesis.

 

[jiwei]

Assuming this DFF was indeed optimized away by Design Compiler, how should I configure my LEC to handle this scenario?

If the flop is a constant 0/1, it can be removed by synthesis. If a flip-flop is redundant, it can be removed by synthesis.

 

[sky_siliconthink]

If you use Formality, it can read in the SVF file generated by DC to help LEC tool understanding the optimization that has been done in synthesis.
If you use LEC from Candence, you may choose to open the *.svf file, check the commands in it and try to find the coressponding command for LEC.

 

[ThisIsNotSam]

I would first start by inspecting the design. A flip-flop being optimized away might be a symptom of a larger issue and might hide bugs.

 

[mmrakshith]

Assuming this DFF was indeed optimized away by Design Compiler, how should I configure my LEC to handle this scenario?

I have also seen many registers being optimized as they are constant. Generally this change should be reflected in the SVF (guidance file) which Formality reads and works it out. Do check if you're reading the right SVFs and if there are one more more make sure you're reading them in the right order.
If some how you've missed to find the register in the netlist, give it another try and check again. Due to some hierarchy change if the path is changed then you might need to use "set_user_match" for both reference & implementation netlists and make sure the register is mapped.