Equivalency Checking Flow – Basics

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.

14 comments on “Equivalency Checking Flow – Basics

  1. walter

    Hi,

    I’m newbie in this field and happens to see your post. Just wonder is that set the naming rule is the only way to mapping signals between designs?
    or is there way to make a 1-1 mapping?

    Reply
    1. Sini Balakrishnan Post author

      Hi Lakshmi
      Could you please give more info on encrypted RTL ? Did you mean IPs from vendor ?
      If the equivalence checking tool is unable to read the content of your RTL, equivalence checking cannot be carried out on that.

      Reply
  2. Aishwarya Singh

    Hi Sini,
    I am running LEC along with power intent for my design. There are level shifters in the design and in the .do file I have mentioned the read of .cpf file. For both the golden and the revised I have added the switch -insert_isolation. Now the issue is that I am getting non-mapped points in both the golden (1) and the revised (3). Due to this issue I am getting non-equivalence. What can be done to remove this issue?

    Reply
    1. Mallikarjun

      Hi Aishwarya,

      Are you doing power aware synthesis?
      If so, you should not apply ‘-insert_isolation’ on revised side.

      Reply
    1. Sini Balakrishnan Post author

      Hi Lakshmi,
      There are two modes in LEC. One is setup and other one is LEC.
      Setup mode is for reading the design files and do compilation & elaboration etc. We need to switch to LEC mode to do Logic Equivalence Checking Operation.
      The command “set system mode LEC” will go to LEC mode from setup mode.
      Hope this is clear.
      Thanks
      Sini

      Reply
  3. Madhu

    In LEC, “set_undefined_cell black_box -both” command will black box modules which does not have module definition. So what is the use of having undefined blackboxes in the RTL design ? Is there any specific reason for which Designer does not add module definitions ?

    Reply
  4. parveen

    How is extra different from unmapped points? In Both of them, compare points are present in one design and not in another one.

    Reply

Leave a Reply to parveen Cancel reply

Your email address will not be published. Required fields are marked *