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.