KEMBAR78
LEC Handout | PDF | Formal Verification | Library (Computing)
0% found this document useful (0 votes)
40 views3 pages

LEC Handout

Lecture handout
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
0% found this document useful (0 votes)
40 views3 pages

LEC Handout

Lecture handout
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 3

Logic Equivalence Checking

Conformal LEC is a tool used for formal verification of designs at various stages in the flow. Formal
verification is the process of verifying designs using mathematical methods. Equivalence Checking is the
process of verifying the correctness of a modified or transformed design (revised design) by comparing it
with it with a reference design (golden design).

 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 Datapath 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

DOFILE
Let us understand the content of the dofile. Dofile is a script file used to run LEC and below is an
example for the dofile.

Below are the basic set of commands used.

 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

39
ASIC Lab Manual
© 2014 Cadence Design Systems, Inc
[Both verilog and liberty format can be used but verilog format is preferred. Steps to generate .v
from .lib using Conformal is mentioned at the end of this session]
 -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

Note: 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.

40
ASIC Lab Manual
© 2014 Cadence Design Systems, Inc
 Generate verification report.
report verification

Reports a table of all violated checklist items

Note: 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.

Note: 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’

41
ASIC Lab Manual
© 2014 Cadence Design Systems, Inc

You might also like