LEC

 

 

  LEC is significant for the designers who need to compare the synthesis netlist with RTL. The most common LEC tools include Cadence Conformal LEC, and Formality. LEC is done  to make sure so that the synthesis optimization and scan insertion do not alter designers intent.Physical designers need to compare PnR netlist  with synthesis netlist, to make sure the PnR results and timing ECOs do not change synthesis netlist functionalities. Designers may perform ECOs for new feature addition and bug fix. There should not be any mismatch between ECO ed RTL and synthesis netlist.

LEC steps

In LEC setup, there are several steps that designers need to follow such as below:

·        Read and elaborate reference design

·        Read and elaborate revised design

We need to specify “notranslate modules” for blackboxing if the module is a macro, or the module has been LEC’ed in block level.

Set certain constraints, for example, when comparing between RTL and synthesis netlist, set case analysis to ignore scan ports.

The next step is LEC key point mapping. In this step, Conformal LEC will first identify primary inputs and outputs, DFF, Latch, Blackboxes, etc. as the key points in reference design and revised design; then pair corresponding reference and revised key points, and perform LEC comparison.

 There are 2 LEC mapping method-name-based and function-based. By default, Conformal LEC will first do name-based mapping, followed by function-based mapping.

In LEC report generation, designers will typically dump the following reports:

·        report unmapped points (-unreachable, -not mapped, -extra)

·        report compare data (-class nonequivalent, -class abort)

·        report black box (check if there’s any unexpected black boxes)

·        report ignored inputs and outputs

·        report pin constraints

·        report output stuck at

·        report floating signals

·        report renaming rule (this guides how LEC performs key point mapping)

LEC non-equivalence debug will be the last step.

Debugging typically starts from unmapped points, and possible root cause includes:

·        Not mapped BBOX pins causes NEQs (Use renaming rule if pins names not matched)

·        Not mapped DFF/DLATCH/CUT/PI causes NEQs (Optimize and merge DFF/DLATCH in LEC

·        Resolve unbalanced loop cutting; Constrain test/scan signals)

·        Incorrect mapping causes NEQs (Remap the incorrectly mapped pairs manually)

After resolving all mapping issues, designers can start debugging real mismatches, and possible root cause includes:

·        Unbalanced floating signals can cause NEQs (Tie off floating pins in RTL, or use “add tie signal” to individually tie each floating Z)

·        Logic optimized differently b/w LEC and implementation causing NEQs

·        Debug phase mapping (Recommended: turn off phase inversion in synthesis; Or auto analysis & remap with phase)

Constraints depend on the stage of LEC.

1. RTL to Pre-scan: no constraints. Just read the design, map and compare.

2. Pre-Scan vs. Post-Scan: Test constraints to mask the test logic. Map and compare.

3. Post-scan vs. Post routed /CTS netlist; No constraints.

do file that is generated after synthesis for doing LEC sufficient to do LEC.Do file is nothing but your own way of generating the commands.

1. Set the log file

2. Read the .lib

3. Read the golden and revised files.

4. Set the mapping rules.

5. Compare.

6. Write the reports.

  If you have automated flow for generating do file for LEC, thats good to start with. If you are using formality for Formal verification, SVF file is useful, where as LEC doesn’t support SVF constructs.

do file commands

Invoke Conformal LEC inside Equivalence checking directory in non-GUI by using the command “lec –xl –nogui -color -64 -dofile counter.do”

 -xl: - Launches Encounter Conformal L with Data path and advanced equivalence checking capabilities

 -nogui: - Starts the session in non-GUI mode

 -color:-Turn on color-coded messaging when in non-GUI mode

 -64:- Runs the Encounter® Conformal® software in 64-bit mode

 -dofile <filename> :- Runs the script <filename> after starting LEC 

Save log file.

set log file <filename.log> - replace

Save log file and replaces if any log file exist with same name if any.

Read the Verilog library by entering:

read library <filename> -verilog –both

Both verilog and liberty format can be used but verilog format is preferred.

-verilog: - to indicate that library is in Verilog format

 -both: - use same library to model or structure both golden and revised design.

 

Read the Golden Design (RTL)

read design <filename> -verilog –golden

 -verilog :- to indicate that RTL is coded in Verilog

 -golden :- to input the golden design

Read the Revised Design:

 read design <filename> -verilog –revised

 -verilog :- to indicate that netlist is in Verilog

 -revised :- to input the revised design

Ignore the scan input(scan_in) and Scan output (scan_out) pins (as these instances are not available in golden design and primary output key point is compare point)

add ignored inputs scan_in –revised [ignores scan_in pin]

add ignored outputs scan_out –revised [ignores scan_out pin]

Constraint the scan enable (SE) pin to zero to keep the revised design in functional mode.

add pin constraints 0 SE -revised [tool keeps the design in functional mode and ignore scan_in pin while compare. Also scan_in is not a compare point]

Change the mode of operation from ‘setup’ to ‘lec’

Set system mode lec

Conformal lec got two modes of operation i.e. SETUP mode and LEC mode. Setup mode is used to prepare the design to be compared. Any command that affects the way the design is modeled will need to be issued in this mode. LEC mode is where the designs will get modeled, key points mapped and where the compare process takes place.

Compare golden vs. revised netlist

add compare points –all

compare

Once the compare process is completed, Conformal LEC will print a summary report that tells how many key points are equivalent, non-equivalent, aborted and not compared.

Generate verification report.

report verification

Reports a table of all violated checklist items

Use command ‘set gui on’ to turn on GUI window.

 In case of mapping issue or comparison issue or not equivalence, use mapping manager or debug manager or Schematic viewer options in LEC to resolve the issue. Same is the flow to compare netlist generated at different stages of physical design. Use proper modelling directives and constraints

Create .v from .lib

Invoke LEC by using the command “lec -xl -nogui -64”

Read library in liberty(.lib) format by using the command “read library <.lib file> –liberty –both”

Write out the verilog file by using the command “Write library <file name*> -verilog”

*file name can be any name with extension .v

Below is a example dofile to generate ‘.v’ from ‘.lib’

Formal verification is same as Logic equivalence checking (LEC) for which the tools are formality by Synopsys and Conformal LEC by cadence. LEC is for RTL vs. NETLIST comparison. Formal verification is for property check.

Formal verification can be classified into 2 types:

1. Logic equivalent.

2. Property check.

Logical Equivalence Checking Netlist vs Netlist problem

Comparing Plain synthesis Netlist vs Low power synthesis Netlist have only used clock gating low power technique. There are unmapped points in Low power netlist - Red coloured "U"-which is of clock gating.Since clock gating is not present in plain synthesis netlist, enable flatten model -clock gating.We should not ignore these. "Plain Synthesis Netlist" Is "Golden" and "Low Power Synthesis netlist" is "Revised" . Also as you have written that you can see the unmapped points at cgc cells. Add the cgc libs cells "Verilog definition" of the cells, at the golden side- from where you are reading all the files and parsing the same. so as to tell the tool to look for these cells and map them.

If you check module by module, then it becomes simpler and in LEC our main motive is that to check whether the flip flops and latches we had made in RTL are required or some extra flops and latches are added which are not required there. Then if this thing is checked module by module then whole process becomes simpler.

In other terms LEC is used to check whether synthesized design(at gate level) which will further go in back-end is according to specification which were written in form of RTL, if we find any mismatch then its clear the RTL logic we had written is not fully according to specification. We can either do a "flat" LEC run which first fully synthesize the design, map it and then compare. Or hierarchical run which compares separately modules and then can copy them to other and save time. If your design is very large you can thing about diving it to sub design or do hierarchical run.

Non-equivalence means that they have different functionality.Unmapped means that Conformal can't find object in Revised design according to rename rules.If your points non-equivalent, check Revised design correctness.If they reported (REPORT UNMAPPED POINTS) as unmapped make something like this :

Do the following to manually map key points:

1. Click the primary output pin in the Golden design to highlight it.

2. Right-click and choose Set Target Mapping Point from the pop-up menu.

3. Click the primary output pin in the Revised design to highlight it.

4. Right-click and choose Add Mapping Point – Non-invert from the pop-up menu.

Modified the netlist to either use input declaration or use supply* for both side.then sign-off by another person, it should be safe enough.

Unmapped in lec

Unreachable means there's no path from that keypoint to a primary output through any sort of logic.Hence they can't have an effect on the behaviour of the design. Conformal by default won't map them nor compare them. The typical causes:

1) unused code in RTL

2) spare gates

3) disabled logic (e.g. pre to post test)

We still like to show you have them though because they could be a problem if they are unexpected.

LEC Mapping and reports

There are 2 LEC mapping method, i.e., name-based and function-based.

By default, Conformal LEC will first do name-based mapping, followed by function-based mapping. This approach typically works really well.

In LEC report generation, designers will typically dump the following reports:

report unmapped points (-unreachable, -notmapped, -extra)

report compare data (-class nonequivalent, -class abort)

report black box (check if there’s any unexpected black boxes)

report ignored inputs and outputs

report pin constraints

report output stuck at

report floating signals

report renaming rule (this guides how LEC performs key point mapping)

LEC non-equivalence debug will be the last step.

Debugging typically starts from unmapped points, and possible root cause includes:

Not mapped BBOX pins causes NEQs (Use renaming rule if pins names not matched)

Not mapped DFF/DLATCH/CUT/PI causes NEQs (Optimize and merge DFF/DLATCH in LEC; Resolve unbalanced loop cutting; Constrain test/scan signals)

Incorrect mapping causes NEQs (Remap the incorrectly mapped pairs manually)

After resolving all mapping issues, designers can start debugging real mismatches, and possible root cause includes:

Unbalanced floating signals can cause NEQs (Tie off floating pins in RTL, or use “add tie signal” to individually tie each floating Z)

Logic optimized differently b/w LEC and implementation causing NEQs

Debug phase mapping (Recommended: turn off phase inversion in synthesis; Or auto analysis & remap with phase)

Balanced but opposite optimization constant

Abort points

Abort Points do come because of large fanin logic cone and if you have not used few RTL rules like using X in RTL.In some cases. You need to figure out first why they have got blackboxed. They are also important.

Blackboxes causes and techniques

Blackbox are produced in following cases:

1)Either you had not provided any basic gate ,common file or you have provided extra file in lec scripts but not included in synthesis (src_design.lst FILE)

2)Either there is problem in your functionality.You just check parametres and null slices in your design.If you find and remove those null slices by changing parametres.Then your blackboxes will automatically removed

After removing BB ,other problems will automatically be removed

Though there are different techniques available like Hierarchical flow, OVF flow, etc., for handling aborts, these have their own limitations. The technique discussed here helps identify common points that have common functionality in the RTL and Gate level netlist.

Adding CUT points at these common points helps to break the huge and complex combinational logic into smaller parts and this eventually helps in reducing the aborts.

The technique is user-friendly and easy to debug, has no Logic Equivalence coverage loss and results in reduced runtime. This technique also has negligible impact on the QoR of Gate-level netlist in terms of area and timing optimization. unique technique to identify CUT points in LEC to resolve Aborts

With increasing design complexities that also incorporate complex data structures there is an increase in the number of aborts in the Logic Equivalence Checker (LEC), which is mainly due to the limitation of the LEC tool in handling the complex logic cone.

Aborts are an inconclusive result that the formal verification tool is not able to resolve. Aborts can be due to:

i)                   Complex datapath;

ii)                  Huge logic cone for comparison; and

iii)                Large number of don’t cares.

The greater the number of aborts in a design, the lesser the LEC coverage and the greater the probability of missing some non-equivalence in a design. Though there are different techniques for resolving aborts, they either involve complex methodologies or a lot of manual processes. It is always imperative that any technique applied should have a shorter turn-around-time, possess minimum LEC coverage loss, and be designer friendly

Adding cut points is a preferred way of avoiding aborts and has an advantage of having no LEC coverage loss. Though the LEC tool itself has the capacity to add cut points at certain points in the combinational logic, the position of these cut points usually are not design friendly. The position of the cut point is necessary in order for a correct comparison and to avoid false non-equivalencies.

 Adding a cut point to the hierarchy actually helps to see same point at the RTL and Gate-level netlist. LEC treats the input and output of the comparison elements separately; hence the input of a cut point is verified during the LEC comparison so adding cut points should not cause any problems. Also, adding a cut point partitions the data path and allows the LEC tool to see reduced data cone and hence be able to resolve the aborts.

 Unmapped points in LEC

Simplest thing is to provide the SVF file from synthesis. This will tell the tool what logic is removed, what is optimized and how its optimized. This resolves most issues.

 

Conformal LEC will first do name-based mapping, followed by function-based mapping. This approach typically works really well.

LEC FLOW

1. file mkdir logical_eq_check

2. set_log_file logical_equivalence_checking.log -replace

3. read_library ../lib/90/slow.v -verilog -both

4. read_design ../rtl/rtl_topmodule.v -verilog -golden

5. read_design syn_report/synthesised_netlist.v -verilog -revised

6. set_system_mode lec

7. add_compared_points -all

8. compare

9. report_messages -compare -verb

10. report_compare_data -noneq

11. report verification

 

In LEC report generation, designers will typically dump the following reports:

report unmapped points (-unreachable, -notmapped, -extra)

report compare data (-class nonequivalent, -class abort)

report black box (check if there’s any unexpected black boxes)

report ignored inputs and outputs

report pin constraints

report output stuck at

report floating signals

report renaming rule (this guides how LEC performs key point mapping)

 

Constraints depends on the stage of LEC.

1. RTL to Pre-scan: no constraints. Just read the design, map and compare.

2. Pre-Scan vs. Post-Scan: Test constraints to mask the test logic. Map and compare.

3. Post-scan vs. Post routed /CTS netlist ; No constraints.

Do file is nothing but your own way of generating the commands.

1. Set the log file

2. Read the .lib

3. Read the golden and revised files.

4. Set the mapping rules.

5. Compare.

6. Write the reports.

If you have automated flow for generating do file for LEC, thats good to start with.
If you are using formality for Formal verification , SVF file is useful , where as LEC doesnt support SVF constructs.

LEC non-equivalence debug will be the last step. Debugging typically starts from unmapped points, and possible root cause includes the below,

Not mapped BBOX pins causes NEQs .Use renaming rule if pins names not matched.

Not mapped DFF/DLATCH/CUT/PI causes NEQs .Optimize and merge DFF/DLATCH in LEC; Resolve unbalanced loop cutting; Constrain test/scan signal.

Incorrect mapping causes NEQs .Remap the incorrectly mapped pairs manually.

After resolving all mapping issues, designers can start debugging real mismatches, and possible root cause includes:

Unbalanced floating signals can cause NEQs .Tie off floating pins in RTL, or use “add tie signal” to individually tie each floating Z.

Logic optimized differently between  LEC and implementation causing NEQs

Debug phase mapping .Its recommended to turn off phase inversion in synthesis. Or do auto analysis and remap with phase.

Balanced but opposite optimization is constant

 

 

Conformal lec got two modes of operation i.e. SETUP mode and LEC mode. Setup mode is used to prepare the design to be compared. Any command that affects the way the design is modeled will need to be issued in this mode. LEC mode is where the designs will get modeled, key points mapped and where the compare process takes place.

Compare golden Vs. revised netlist

add compare points –all compare

Once the compare process is completed, Conformal LEC will print a summary report that tells how many key points are equivalent, non-equivalent, aborted and not compared.

 

Generate verification report.

report verification

Reports a table of all violated checklist items

Use command ‘set gui on’ to turn on GUI window. In case of mapping issue or comparison issue or not equivalence, use mapping manager or debug manager or Schematic viewer options in LEC to resolve the issue.

Same is the flow to compare netlist generated at different stages of physical design. Use proper modelling directives and constraints

Create .v from .lib

 

Logical Equivalence Checking Netlist vs. Netlist problem

 

Comparing Plain synthesis Netlist vs Low power synthesis Netlist have only used clock gating low power technique. There are unmapped points in Low power netlist ( Red coloured "U") which is of clock gating. Since clock gating is not present in plain synthesis netlist. i have enable flatten model -clock gating.

We should not ignore these. "Plain synthesis Netlist" is "Golden" and  "Low Power Synthesis netlist" is "Revised" .

Also as we have written that we can see the unmapped points at cgc cells. add the cgc libs cells "Verilog definition" of the cells, at the golden side- from where you are reading all the files and parsing the same. so as to tell the tool to look for these cells and map them.

Perform equivalence checking between RTL and gate-level netlist

If we check module by module, then it becomes simpler and In LEC our main motive is that to check whether the flip flops and latches we had made in RTL are required or some extra flops and latches are added which are not required there. Then if this thing is checked module by module then whole process becomes simpler.

In other terms LEC is used to check whether synthesized design(at gate level) which will further go in back-end is according to specification which were written in form of RTL, if we find any mismatch then its clear the RTL logic we had written is not fully according to specification.

We can either do a "flat" LEC run which first fully synthesize the design, map it and then compare. Or hierarchical run which compares separately modules and then can copy them to other and save time.
If design is very large we  can think of going  to sub design or do hierarchical run.