Logical Equivalence Check

LEC consists of three steps: Setup, Map and Compare.

Setup:

In setup mode, LEC reads in two netlists , one synth netlist and one apr netlist. For execution, LEC needs three files.

  • .lec file guide the Conformal tool to execute different command in a systematic way.
  • scan_const file provides scan related constraints like if we want to ignore some scan connections/serdes input/output pins which are defined in this file.
  • stdlib file contains pointer of standard cells library.

In the transition from setup mode to LEC mode, the Conformal tool flattens and models the golden and revised designs and automatically maps the key points. The key points are defined as:

  • Primary Inputs.
  • Primary Outputs.
  • D Flip-Flops.
  • D Latches.
  • TIE-E Gates (error gate, created when x-assignment exists in revised design).
  • TIE-Z Gates (high impedance or floating signals).
  • Black boxes.

Mapping:

There are two types of mapping methods one is name based mapping one is functional mapping. By default, tool does name based mapping. If there are any unmapped points, tool reports it as:

  • Extra unmapped points are key points that are present in only one of the designs, Golden or Revised.
  • Unreachable unmapped points are key points that do not have an observable point, such as a primary output.
  • Not-mapped unmapped points are key points that are reachable but do not have a corresponding point in the logic fan-in cone of the corresponding design.

Compare:

After the Conformal tool maps the key points, the next step of the verification is comparison. Comparison examines the key points to determine if they are equivalent or non-equivalent. The comparison determines if the compared points are:

  • Equivalent.
  • Non-equivalent.
  • Inverted-equivalent.
  • Aborted. We can also do with upf and without upf comparisons.

If there are any non-equiv’s check the reports for non-equiv and unmapped.

Written on September 21, 2020