Mapping points or KEY points in Logic Equivalence Check
Key points in LEC or mapping points in LEC, as it often called, are the most important points in Formal verification as all the verification revolves around them. Let us first list out all the Key points in LEC or mapping points in LEC.
- D Flip-flops
- D Latch
- Black Box(BB)
- Primary Inputs(PI)
- Primary Outputs(PO)
- Tie-E Gates
- Tie-Z Gates
- Cut gates
Note: To read about logic equivalence check:
As I have described the basics of LEC in my last article, Logic Equivalence check is done between golden designs and revised designs. The above key or mapping points are used as a reference by the LEC tool to compare points in both revised and golden designs.
Now, the question is where these Key points are located in the designs? So, as we know all the logics are being computed by the combinational logics, and we want to verify whether the logic computed by the combo logic is correct or not in the revised design. This combo logic is confined by these Key points as shown in the figure 1.
As soon as LEC tool reads the golden and revised designs along with all the required library the next thing it does is mapping of the key points that is why we often call them as mapping points. Tool maps same kind of key point in both golden and revised designs, it cannot map different kind of key points with each other.
We can map DFF in the golden design with the corresponding DFF in the revised design. DLatch, PI, PO and BBOX are mapped with the corresponding their key points in revised designs.
Tie-Z gates are created by the tool at the time reading the designs. There may be some floating nets and pins in the design, while tool reads these kind of designs it creates tie-Z gates at floating nets and pins. It also creates tie-Z gate while modelling a tristate.
Tie-E gates: If there may be some x-assignments in the design, tool represents them as a don’t care in golden design and tie-E gates in revised design.
Cut gate: If there is any combinational feedback loop in the design, tool will not be able to compare or handle it. Tool will break that combinational loop by inserting a cut point that is called as a cut gate. Tool will then map this cut gate from golden design with the corresponding cut gate in the revised design.
Once mapping is done tool will compare the two designs with the help of compare points. If all the compare point values is equal in both the designs, it will give a result as PASS otherwise NON-Equivalent.