Logic Equivalence Check: ASIC design cycle involves a number of stages that vary from functional design to its verification at different levels. As soon as the design is completed and verified through different methodologies is ready to go to a semiconductor chip. Hold on, it’s not simple as it said, one of the most crucial steps is involved while taking RTL design to the chip level. Synthesis, which involves the conversion of RTL design to the equivalent gate-level netlist. This netlist is then used for the physical design implementation.

Once the netlist gets generated it is must to ensure that its functionality is equivalent to the RTL design from which it has been generated. The logical equivalence check performed to ensure the logical equivalency of the gate level Netlist with the RTL design. It can also be performed to check the equivalence of the:

• Netlist to Netlist
• Library to Library

A number of EDA companies provide equivalency check tools out of them Formality (Synopsys) and Conformal (Cadence) and mostly used at the industry level.

Inputs to the Logical equivalence Check are:

1. Reference Design: It also called the golden design for process. It is used to compare the design which is to be checked for the equivalence. Functionality of the design which is checked must be functionally equivalent to this design (i.e. RTL).
2. Implemented Design: It is the design which is going to be checked for the equivalence (i.e. Netlist).
3. Library: The library files are needed because the netlist has been generated using these files.

Steps involved in Logic Equivalence Check:

1. Read: This step involves in reading of the implemented, reference design and the Library files. Here, the design gets converted to the logic cones which can be used for the compare points in later steps.  Logic cone is consists of the combinational logic generated from the reference or implemented design. It also shows the connecting ports for the particular logic which are used as the compare points. The connecting ports can be connected to any register, wire or black box.
2. Match:This step involves in the matching or mapping compare points from the reference and the implemented design. Compare points for LEC are Primary outputs, Sequential elements and Black box input points.
3. Verification: In this step toll verifies whether the compare points are proven for functional equivalence or not.
4. Debug: The debug phase begins when the tool has returned a non-equivalent result. The logics then improved with the help of LEC tool and again Checked until they become logically equivalent to the reference design.

The issues and the debugging process:

Most of the challenges and the problems are faced in the process are due to logic optimization at the Synthesis stage. The netlist generated during the Synthesis process is finalized after number of process iterations to meet the Timing and Design constraints. These optimizations involves in removing of unused sequential elements and also merging of the sequential elements. As in comparison to the RTL, the netlist can posses different properties if it get generated with clock gating or scan enable sequential elements. One must be look after these main points while doing formal verification:

1. Complete inputs information:The first thing first, the verification person must have all the input information used at the time of the Synthesis. One must be careful about these things at the time of setup.
   • Reference Design: All the standard cell libraries, all the macro libraries(if any). If your reference design is RTL then all the modules or pieces of the design.
   • Implemented design: Here also, All the standard cell and macro libraries be used which were used initially.
2. Setup files: The file needed to inform the tool about the design transformation or modification during optimizations. Formality from Synopsys provide .svf file for this setup information, one need to include this file while verification.
   • Removal of the unused Flip-Flops
   • Merging of the FFs
   • Register optimization
   • Datapath optimization
   • FSM re-encoding
3. Clock Gating:It used to reduced the dynamic power when circuit do not required to change their states unnecessary. This is done by adding extra circuitry in the clock path, this added logic lead to a mismatch during verification. To avoid this problem, Formality use ” set verification_clock_gate_hold_mode low“ command.
4. Scan Flip-Flops: Scan flip-flops are inserted for the DFT process after replacing the flio-flops. These are used by a design for manufacturing test. The extra logic in the path of data pin leads to logic cone match fail. To avoid this problem Formality uses a “set_constant” command to disable the scan functionality by selecting the data as input instead of scan input, “set_constant i:/WORK/TOP/test_se 0“. 
5. ECO Changes: ECO is done by manually modifying netlist with swaping cell, sizing cell or inserting buffers. These modifications in the netlist which were done to improve timing may lead to alter the logic. Suppose you have up-sized a cell to fix the setup time violation or inserted a buffer to fix hold time violation. LEC is done to ensure these modifications has not effected your functionality.