Once RTL is released, the next step is to go for synthesis to get a gate-level representation of the design. This is called synthesized netlist. Assumption is that synthesized netlist has the same functionality as the RTL. Equivalency checking comes into picture to make the assumption into a conclusion.
Equivalency checking tool compares RTL and netlist and points out the functional differences if any, otherwise they are reported as equivalent. If the synthesized netlist if equivalent to the RTL, place and route will be done and a post-layout netlist, (aka. pnr netlist) will be dumped out. Here again Equivalency checking comes into picture. EC tool will make sure that pnr netlist has the same functionality as the synthesized netlist. Thus EC tool always works on two inputs and compares whether they are functionally equivalent or not.
As the tool always compares two inputs, one is considered as golden and other is revised. For equivalence check between RTL and synthesized netlist, RTL is considered as golden as all functionality implemented has been verified by other methods like simulation, assertion based verification etc. Formal EC can tell revised design(In this case, synthesized netlist) has the same functionality as golden or not.
Following are the general steps involved in RTL vs synthesized equivalency checking.
In Setup Mode:
Read & Elaborate Golden Design: In this stage, both library and golden design information has to be passed to the tool. For Conformal LEC, this would be done by using the commands like read library, add search path, read design etc. Once all are read in, next step is to do elaboration. Elaboration stage will give warnings/messages about missing files, unsupported constructs etc. You may need to fix those issues. Some of the unsupported files would come as blackboxes, like RAMs/memories etc.
read library -Liberty -both
add search path . /opt/synopsys/dc_G-2012.06-SP3/packages/dware/src/ read design -verilog2k -noelaborate -golden -f filelist read design -vhdl 93 -noelaborate -golden -f filelist.vhd elaborate
User can add black boxes by using `add black box` command. Those will be the user defined black boxes. Mixed languages support is available in most of the equivalence checking tool. LEC supports Verilog, system Verilog, vhdl and liberty files.
Read & Elaborate Revised Design: Exactly like in the previous step, the information about the library and revised design (netlist) has to be passed to the tool. Once the netlist is read-in, do elaboration and set the black boxes.
Black box Report: Black boxes have to be matched for golden and revised to proceed further. So do `report black box` to get the details and manually check them. If these are same in golden and revised, we can go to the next step.
report black box -detail
Set scan constraints: If the netlist is a scan inserted, RTL vs Netlist comparison has to be done by disabling scan path. To do this, use add pin constraints and add ignore outputs commands.
add pin constraint 0 scan_enable_i -both add pin constraint 0 scan_mode_i -both
Set flatten Model : Usually synthesis does lots of optimization. This will differ as per the requirement. So first try to understand what all optimization has been carried out during synthesis, which helps in setting the flatten model for equivalence checking. Some of the examples are sequential constant , sequential redundancy etc. Detailed information will be available in the upcoming sessions.
set flatten model -seq_redundant -seq_constant -gated_clock
Equivalence Checking Mode:
Next step is mapping and comparison. This can be done only in equivalence checking mode mode. So change mode to LEC as per Conformal LEC tool.
While moving from setup to equivalence checking mode (LEC mode), it flattens and models the golden and revised designs and do automatic mapping of key points. Key points are defined as Primary Input and Output, D flip-flops and latches, TieE & TieZ gates and blackboxes.
If the name based mapping is not complete, user can go for re-naming rules or request the tool to do functional mapping.
Sample renaming rules add renaming rule X1 "\/_" "\/X" -golden add renaming rule X2 "_\/" "X\/" –golden
Functional mapping command set mapping method -name first
Final unmapped points are classified in extra, unreachable and not-mapped. Extra means, it is present only on one designs. Unreachable means these key points do not have an observable point. Unmapped key points are reachable but do not have corresponding key points in the other design.
Once mapping is clean, that means there are no unmapped key points, or unmapped key points present only in the golden, we can go for comparison. Comparison checks whether these compare points are equivalent or not and report as equivalent, non-equivalent, inverted equivalent or aborted.
add comp po -all compare
If the compare points are non-equivalent, user has to go for diagnosis to find out the differences. Most of the tool precisely locates the cause of a non-equivalent point and come up with the error patterns that lead to the failure. Also the tool will dump out the possible candidates.
In Conformal LEC, command analyze non-equivalent and analyze setup helps the tool to analyse the root cause and act accordingly. For aborts, data path analysis helps. But go for abort resolution once there are no non-equivalent key points in the report.