verplex
- Details
- Last Updated: Wednesday, 01 May 2019 13:35
- Published: Wednesday, 01 May 2019 13:35
- Hits: 2468
Verplex was formal verification tool developed by Verplex in 1998. Cadence acquired it in 2003, and developed it under Conformal family of tools. Conformal family of tools are:
- Conformal LEC: formal verification tool (similar to formality by Synopsys). It has basic to advanced tools starting from Conformal L, Conformal XL to Conformal GXL.
- Conformal Low Power: enables low power equivalence and func checks for isolation cells, level shifter cells, state-retention cells.
- Conformal Constraint Designer
- Conformal Custom
- Conformal ECO Designer (look in eco.txt to see how to use conformal for eco)
Conformal LEC:
--------------
Encounter Conformal (EC) Logical equivalency checker (LEC): verifies RTL, gate or transistor level design
--------------------------------------
4 variants of conformal:
Conformal L (basic LEC), XL (extends to datapath synthesis/layout), GXL (extends to custom logic/memories), LowPower(includes equivalence and functional checks for isolation cells, level shifter cells and state retention cells).
Conformal LEC is 3 step process:
1. Setup mode: Read in golden and revised design and their associated library. Designs can be in verilog/vhdl, while libraries can be as verilog library or as Liberty files. Then we specify constraints and other parameters. All these designs/libraries are translated into conformal primitive gate types, which are: AND, OR, MUX, BUF, XOR, DFF, DLAT, INV, ADD, MUL, SUB, TIE0, etc (about 100 primitives). Most of these primitives are same as those of verilog.
2. Transition from setup to LEC mode: conformal checks various rules during parsing, and reports all of the library and design rule violations that occurred during parsing. Then it flattens and models the Golden and Revised designs and automatically maps the key points.
Key points are defined as Primary Inputs(PI), Primary Outputs(PO), D Flip-Flops(DFF), D Latches(DLAT), Blackboxes(BBOX), TIE-E Gates(E:error gate, created when x-assignment exists in Revised design), TIE-Z Gates(Z:high impedance or floating signals), Cut gates(CUT:artificial gates that break combinational loops).
3. LEC mode: Conformal does mapping of key points and reports unmapped points. Then it compares these mapped points (PO, DFF, DLAT, BBOX, E, Z, CUT but NOT PI) to determine if they are equiv or not. Each Key point may have multiple pins, and when checking for equivalence, all of these pins have to be equiv for that key point to be equiv.
We can also designate mapped points for comparison manually by adding naming rules. 2 ways of comaparison:
A. Hierarchical comparison: if one of the 2 designs is RTL.
B. flattened comaprison: done when both designs are gate level
Mapping is of 2 types: Needs to be set before exiting setup mode. Default is name based mapping.
A. name based (automatic) => 3 name based mapping:
I. name first mapping: first maps key points with same name, and then remaining key points with mapping algorithm. Any remaining points are identified as unmapped points.
II. name guide mapping: it does the opposite of name first. It first maps key points with mapping algorithm, and then remaining key points by matching names. Any remaining points are identified as unmapped points.
III. name only mapping: maps points only if names match. Any key poitns that don't have same name are identified as unmapped points.
B. non-name based: Doesn't involve names. 1 type of non name based mapping:
I. no name mapping: relies solely on mapping algo to map key points. Any remaining points are identified as unmapped points.
name based mapping is preferred as the name effort (set in the SET MAPPING METHOD command) is high by default and can take care of most changes in delimiters.After name-based mapping is performed, the left over key points will have different names between the Golden and Revised designs. There are several ways you can make their names similar in both designs:
1. Naming rules => Naming rules will be applied in RTL and facilitates in name based mapping with netlist
2. Renaming rules => Renaming rules are applied when the instance names are different in golden and revised however shares a common pattern.
3. ADD MAPPED POINTS command => When the number of key points having different names do not have common pattern and are less in number then it is good to manually map those key points using add mapped points command.
Number of key points b/w golden and revised may be different. Tool maps same key points b/w the two. Any kep points still not mapped are classified as unmapped points. Unmapped points are classified into 3 types (each type may have key points from DFF/DLAT, E, Z, etc):
1. Extra unmapped points (E): key points that are present in only one of the designs,Golden or Revised. This E is different than E of key points which stands for Error key points.
2. Unreachable unmapped points (U): key points that do not have an observable point, such as they do not propagate to a primary output or other key points.
3. Not-mapped unmapped key points (shows as Red DOT): key points that are reachable but do not have a corresponding point in the logic fan-in cone of the corresponding design. For complete mapping, there should not be any of these. These will be need to be resolved before running compare. Once we have 0 "Not-mapped" unmapped key points, we should report all unmapped points, and make sure they are expected as either E or U.
Compared points may be equiv, non-equiv, inverted-equiv or aborted. There should be no non-equiv points for a passing design. In the case of aborted compare points, you can change the compare effort to a higher setting. Thus, Conformal can continue the comparison on only the aborted compare points.
NOTE: For the whole design, all PI, PO, flops, latches and BlackBox are mapped. Points that still remain unmapped may be due to spare flops in revised, optimized away flops that are present in RTL but not in revised, BlackBox of antenna diodes in revised, etc. Any other unmapped points will need to be mapped. If they remain unmapped, then that may indicate some real flops missing in revised. Once all points are mapped (except for unmapped points, we set compare points which are PO, flops, latches and BlackBox. If they all match, then designs are equiv, else non-equiv
Renaimg rules: Add renaming rules if names don't match, and we want to force the tool to map certain key points.
-------------
add renaming rule d2D '/d$' '/D' => adds a renaming rule "d2D" which renames small d to capital D.
add renaming rule r1 {"_reg_%d"} {"_reg[@1]"} => maps _reg_1 to _reg[1]
test renaming rule fsm_state_reg_2/N01 => this tests rules against the specified object and shows the renamed result.
Conformal supports 2 types of tcl cmd:
1. native tcl cmd (not as efficient as internal C funstions). entered by typing "tclmode" on cmd line. prompt shows TCL_*>.
ex: TCL_*> set env(RC_VERSION) "RC10.1.200 - v10.10-s202_1" => tcl cmd entered while prompt shows TCL_*.
2. Conformal tcl cmd (which have been tailored for use with Conformal to query the design database. Information retrieved from the design database is referenced by pointers (which are also called object handles in Tcl)). entered by typing "vpxmode" on cmd line. prompt doesn't show TCL_ anymore, so it means it's in vpx mode.
dofile syntax:
------------
1. // comments out rest of the cmd, while /// comments out rest of the line
ex: //read library lib_01.lib \
lib_02.lib lib03.lib => here all of the cmd is ignored (1st line as well as second line)
ex: read library lib_01.lib \
lib_02.lib /// lib03.lib => here only lib03.lib is ignored. Rest of the cmd read lib01 and lib02.
2. Directives: We can enable/disable specified synthesis directives when reading in verilog/vhdl files. All directives by Cadence, synopsys, ambit are enalbled by default
add conformal directives as "infer_latch", "multi_port", "clock_hold", etc in the comment line //.
set directive off synopsys => this disables all synopsys directives found in verilog. We can use "on" to enable directives. If we don't provide vendor name as "synopsys" or other vendor name, then option applies to all vendors.
set directive off => disables all directives
set directive on parallel_case => enables only parallel_case directive since all other directives have been turned off.
Conformal lec run:
----------------
In main dir, we can have startup file .conformal_lec (it can be in installation dir, home dir or current dir) that conformal will execute on startup. The cmd files that are run are called dofiles. dofiles can be used at startup by specifying -dofile option
lec -12.10-s400 -nogui -log ./logs/rtl2gate.log -dofile scripts/rtl2gate.do => without -xl or -gxl, default Conformal L is started.
lec -9.1 -xl -nogui -log ./logs/rtl2gate.log -dofile scripts/rtl2gate.do => -xl needed for running dofile from RC.
lec -13.1-s180 -xl -nogui -log ./logs/rtl2gate.log -tclmode cmd.tcl => here instead of do file, we use tcl file
NOTE: starting from lec -13.1 and upto x.y, all cmds below are not separate (i.e read library), but joined by _ (i.e read_library). However, from 15.x onwards, cmds are back to original way (w/o _).
NOTE: we can start lec in gui mode by omitting -nogui
rtl2gate.do:
----------
0. set system mode setup => optional, as by default it's in setup mode (in later versions, all connected by "_", "set_system_mode setup").
1. Read library: It reads library in liberty format (since liberty files are used during synthesis). It can also read simulation library in verilog format, but only V-1995 format is supported. Simulation libraries should be used for final equiv check, since design verification signoff happens with simulation libraries, and NOT with synthesis libraries.
#-statetable option applies with liberty files, and specifies that library contains state tables.
#-both says read these libraries for both golden and revised. Else put -golden or -revised.
read library -statetable -liberty -pg_pin -both \
/db/pdk/.../src/MSL270_W_125_2.5_CORE.lib \
/db/pdk/.../src/MSL270_W_125_2.5_CTS.lib \
/db/pdk/.../src/edc01024064012_W_125_2.5.lib => if fram or other ip are there
#read library -both -sensitive -Verilog /db/pdkoa/lbc7/2012.05.07/diglib/msl270/verilog/models/*.v => reading simulation library. sensitive means make it case sensitive
#read library -verilog -both lib/*.v fram.v => to read verilog simulation library
#NOTE: sometimes .lib and .v library for cells are not equiv at TI for some of the cells. In such case, first validate that the two libraries are same so that there is mismatch b/w lec and rtl sim resuls. Run these 3 steps to do that in a separate script.
read design -golden -verilog -define TI_functiononly -replace /db/verilog/models/*.v
read design -revised -liberty -append /db/pdk/.../src/MSL270_W_125_2.5_CORE.lib
validate library => results show all cells and whther they are equiv or not b/w verilog and liberty
2. Read RTL design: Read rtl, elaborate and set top level to digtop
#-lastmod specifies that use the last module found incase of duplicate modules (default is to use the first module found and ignore other duplicate modules)
#-noelab should be used when design contains mixed languages. We want to do elaboration separately, as doing it with the read design cmd might fail to resolve it appr.
#-keep_unreach => unreachable key points are preserved. This is needed when hdl_preserve_unused_registers attribute is true on RTL designs.
#-map or -mapfile option allows designs to be stored in named workdspace isntead of default "work" workspace.
#-rangeconstraint and -configuration only applies to vhdl files. -rangeconstraint causes "dont care" for attributes when a variable is out of range. -configuration causes conformal to link entity/architecture giving configuration higher prority than lastmod.
read design -rangeconstraint -configuration -vhdl 93 -golden -lastmod -noelab \
../../Source/spi_typedefs.vhd \
../../Source/spi.vhd
#read design -verilog top.v -golden => read verilog design separately (-verilog2k for V2001)
#read design -file golden.vc -golden => golden.vc file has all verilog files in it as:
#-y Source/* => all files in this dir read
#golden1.v => other verilog files to be read
NOTE: when using golden.vc, sometimes digtop cannot be reolved as top level module, so we'll need to specify "digtop" and "defines" file separately
#write design => used to wrt out the design in verilog format that was read in. Useful to learn how Conformal parses RTL.
#elaborate design -golden => not needed as design is already elaborated by default.
set root module digtop -golden => here we can set root module to some lower level also, in that case comparison will start from that module. useful during hier comparison.
3. Read Synthesized gate level design, and set top level to digtop (no elaboration needed for gate level design):
read design -verilog -revised -lastmod netlist/digtop.v \
elaborate design -revised
set root module digtop -revised => here we can set root module to some lower level just as can do it for golden above.
4. reports: rule check report below is a must for any RTL/gate neltist to make sure all of these warnings are OK. When RTL is coded for the first time, running verplex on RTL and reporting rule check is done to find any errors in RTL. These reports are also shown by default.
report rule check -all -verbose -design -golden => this reports all warnings/errors on golden RTL
report rule check -all -verbose -design -revised => this reports all warnings/errors on revised netlist
report design data => to run report of current design info. displays number of design modules, library cells, inputs, outputs, primitives, and one-to-one mapped state points on the Golden and Revised designs
report black box => To see what modules/cells got reported as black box. There should be none
5. set parameters
##add blackbox for IP/Macro. By default, blackboxes are mapped by their module names. To map by instance names instead, use the "SET MAPPING METHOD -nobbox_name_match" command. 3 ways:
A. add notranslate module : run before reading in design or library (before step 1 above). This is used for memories, since here the actual code of module is not parsed, but only dir for I/O ports are parsed and used for blackbox. This saves computer memory from reading and comparing these huge memory modules. ex: add notranslate module -both sshdbw00056025020 => this sram module treated as blackbox for both golden/revised.
B. add black box : run after module has already been read in. Used during hier comp.
C. set undefined cell -black_box : run before reading in design or library. this is useful if module doesn't exist at all. It tells Conformal to treat missing ref as blackbox. First 2 cmds above require code (may be empty code) for module with port declarations (conformal uses input/output dirn), while this one doesn't.
add black box fedc01024064012 -revised => module name and NOT instance name. No hier as it's flat in gate verilog. Ideally we should add black box for both RTL and gate by using option -both.
#add black box /U1/U4 -module -Golden => U4 module inside top level U1 module. If -module not used, then provide instance name
#reports if blackboxes are paired correctly b/w RTL and gate.
report black box -detail => use -detail to get detailed info.
##add net/pin constraint (only needed for scan designs):
add pin constraints 0 scan_en_in -revised => to force scan_en_in to 0 for gate netlist (since scan_en_in not tied to anything in golden RTL). If scan_en_in is not forced to 0, then gate netlist will have all flops which have extra scan_en pin, and when scan_en_in=1, then RTL and gate flop logic will mismatch.
#add pin constraints 0 scan_mode_in -both => This is needed since synthesis adds an extra mux on the output of final scan_out flop to give out diff o/p during scan_mode. However, we should run the tool with this commented out, so that we can be sure that the sdo_out port is the only one that is mismatching. Then we can uncomment this constraint, and run LEC again, which should be clean. Since scan_mode_in is just like any other i/p pin, blindly setting it to 0, may mask real logic problem which might have happened during synthesis.
NOTE: ideally, we should not constrain any pin for scan design. There are 4 possibilities of scan_en and scan_mode combo:
1. scan_en=0, scan_mode=0/1: This is above constrain that we already have. Only mismatch should be SDO out (when se=0, sm=1). For newer designs, tool puts mux at o/p pin SDO whose select pin is tied to se instead of sm. So, for se=0 (sm=x), designs would be lec clean since SDO would be matched for se=0, sm=x. If select pin of mux was tied to sm, then SDO out won't be equiv b/w gate and rtl.
2. scan_en=1, scan_mode=0 : This constrain can be put only for newer designs which don't have scan_en and scan_mode as PI ports. Since Internally scan_en is turned off whenever scan_mode=0 (there's "AND" gate logic), this becomes same as above (se=0,sm=0). Should pass with no mismatches. It's important to check this case as we may have design where during synthesis, we incorrectly set PI pin as se pin (instead of setting o/p of and gate as se pin, where 1 pin is PI and other pin is sm). In that case lec may never catch this bug if we don't check for this constraint (se=1, sm=0). silicon will never work with this bug, as during func run even when sm=0, toggling PI pin will cause se pin of each flop to toggle causing incorrect behaviour.
NOTE: for older designs which have scan_mode and scan_en i/p and o/p pins tied together at top level, we may not be able to run lec to test this case. However, it's already tested, as o/p pin scan_en_out is already tested in case 1 above (se=0, sm=0/1) for LEC as it's PO. So, no way that bug for option 2 can appear for older designs w/o causing LEC mismatch in scenario 1 above.
3. scan_en=1, scan_mode=1 : This will have all flops as non-eq, since flops in rtl do not have se pin, so this case can't be tested.
We should set these 2 cases (1 and 2 above) shown above in separate runs, and make sure they are clean. Just checking for se=0, sm=0 doesn't check all possible logic for scan.
NOTE: In newer designs, we don't have scan_en_in and scan_mode_in as separate PI ports. Since constraints can only be applied to PI pins, we have 2 options to get it to work:
1. we set root module to the sub-module which has this pin as the i/p pin to that sub-module. Then we can add pin constraint to that pin as it's a PI fo that module. Then we switch back to top level module.
Ex: to set scan_en_in to 0, and make scan_en_out as PO. This makes the design same as older designs where scan_en_in i/p was constrained to 0, while scan_en_out was PO.
set_root_module u_dig_test_1 -revised => we provide module name and NOT instance name
add_pin_constraints 0 test_se -revised => add pin constraint to scan_en pin to that submodule. Do it for other submodules too whose scan_en i/p pin need to be tied to 0 (by setting root module to that submodule).
set_root_module DIG_TOP -both => switch back to top level module to do comparison once all sub-module pins have been constrained
add_primary_output u_DIA_DIG/scan_enable -both => we add "scan_en" o/p of sub-module as PO so that it can be compared. If we do not do this, then "u_DIA_DIG/scan_enable" may become Z(f) pin, which will not be compared. This pin will now show up as PO for key point mapping purpose.
2. Most of the times, scan_en and scan_mode are o/p pin of submodule (and not i/p pin). They do go as i/p pin to various other sub-modules, but then we have to do add_pin_constraints to i/p pin of each sub-module (at too many places), so, option 1 above may not work efficiently. Instead we can cut o/p ports of such submodules, and make them PI and then constraint them. It achieves the same result as option 1 above, but is much easier.
Ex: same as option 1 where it looks the same as older designs.
add_primary_input "u_SPT_DIG/auto/Scan_En" -net -cut -both => o/p pin of "auto" module is made as PI. -pin says it's a pin, while -net says it's a net (net is default). -Cut cuts the other original drivers and allow only the newly added primary input as the driver of the net or pin. This is the default. -NOCut does not cut the other original drivers, so new net gets driven by both internal as well as external driver (becomes a wired net). In this ex, "u_SPT_DIG/auto/Scan_En" net becomes a floating net, and all connections to this net, now get driven by PI pin "u_SPT_DIG/auto/Scan_En" which is a new user defined PI.
add_pin_constraints 0 "u_SPT_DIG/auto/Scan_En" -both => as this pin is PI now, we can add constraint now. Note: once a constraint is added on a PI, it doesn't show up as PI anymore, as it's not used for mapping (since it's a constant pin)
add_primary_output "u_SPT_DIG/auto/Scan_En" -both => we add "scan_en" o/p of sub-module as PO so that it can be compared. This pin will now show up as PO. This pin is defined both as PI and PO. That's OK as bidir ports are also defined that way. Also, it doesn't show up as PI anymore as it's a constrained pin.
add pin equivalences CLK CLK1 -revised => clk in RTL got trnslated as 2 pins CLK and CLK1 in gate. So, CLK1 is declared same as CLK.
add primary input net1 -net -revised => to add net1 inside revised netlist as extra PI to gate netlist
add primary output net2 -revised => to add net2 inside revised netlist as extra PO to gate netlist
add tied signals 0 SO -net -module U1 -revised => to tie floating nets/pins to 0/1
add instance constraints 0 /TOP/U2 => To constrain any internal DFF or DLAT output to Logic-0 or Logic-1
add instance equivalence U1 U2 -Golden => to specify internal equivalence or inverted equivalence between DFFs or D-Latches.
add cut point /U1/net1 -revised => To specify the cut points for breaking combinational feedback loops (conformal automatically cuts the loop when we exit setup mode)
report_pin_constraints -all => This is to verify that only intended constraints are there. Very important to run this.
#set flatten model => this cmd allows you to specify certain conditions for flattening the circuit. Usually applies to revised, when conformal is flattening design, as revised netlist is the one which get these transformations added by synthesis tool. (-latch_fold is the only option that should be needed. all others are optional).
#set flatten model -map => conformal automatically maps key points when it exits the Setup mode
set flatten model -gated_clock => when clk gating causes problems during comparison, we use this cmd to remodel latch based clk gaters into mux based feedback ckt to match rtl. adding option "-gated_clock_latch_free" remodels latch free clk gating into mux based feedback ckt. However, for this modeling to be valid, enable signal must be stable while clk is active.
set flatten model -latch_fold => To convert two master/slave D-latches (DLATs) into a single D flip-flop (DFF) gate. NOTE: This important to provide, since most libraries model flops as 2 MS D-latches while in RTL they are FF, so it will give tons of unmapped points when running lec with verilog model library, since DFF in RTL can't map to DLAT in libraries.
set flatten model -latch_transparent => to remodel DLAT (whose clk ports are always enabled) into buffers (transparent latch)
set flatten model -seq_merge => To merge common groups of sequential elements as one sequential element in the clock cone of a DFF or DLAT
set flatten model -all_seq_merge => same as above except that it's for the logic cone. -all_inv_seq_merge is for elements that are inverted.
set flatten model -seq_redundant => To remove seq redundancies, as rst pin of flop anded with Q o/p pin of flop. This redundancy causes non-eq for designs, so important to set this. At TI, verilog models of lib cells have this redundancy (SDB20.v in 33hpa07) in some cells, so we use option "-lib_seq_redundant" to remove redundancy from lib cells. In order to pass lec, we will have to use this option "set flatten model -lib_seq_redundant -seq_transform", run compare (which will show non-eq points), then do "analyze noneq" and agian run compare, which will make designs lec clean.
set flatten model -seq_Constant => To convert a DFF or DLAT to a ZERO/ONE gate if the data port is set to 0/1. adding option "-seq_constant_x_to 0" to -seq_Constant option will optimize flop to constant value 0 when flop is always in "X" state.
set flatten model -loop_as_dlat => To model combinational loop as a DLAT.
#mapping method: needs to be set before exiting setup mode. Default mapping is name-first, with no case sensitivity (use -sensitive to make it case sensitive).
set mapping method -phase => This method maps the key point with an inverted phase. i.e. comapres set logic of gloden to reset logic of revised and vice-versa for inverted-equiv. Phase mapping is recommended when the synthesized netlist has gone through sequential inversion or inverter push.
set mapping method -unreach => To map unreachable points.
#report environment -mapping => reports mapping method used.
set directive off synopsys => turn off synopsys directive
6. set lec mode, compare and report results:
set analyze option -auto
set system mode lec => This starts the mapping b/w golden and revised key points
=> At this point, all key points for golden/revised are reported, and which of these are mapped/not-mapped.
// Warning: Golden and Revised have different numbers of key points: Golden key points = 5379 Revised key points = 5238
// Mapping key points ... Warning: Golden has 8 unmapped key points
================================================================================
Mapped points: SYSTEM class
--------------------------------------------------------------------------------
Mapped points PI PO DFF DLAT Z BBOX Total => Z means floating node (TIE-Z)
--------------------------------------------------------------------------------
Golden 205 609 4302 104 7 4 5231 (total golden key points =5231+106+34+8=5379, matches above. see below)
--------------------------------------------------------------------------------
Revised 205 609 4302 104 7 4 5231 (total revised key points =5231+7=5238, matches above. see below)
================================================================================
Unmapped points:
================================================================================
Golden:
--------------------------------------------------------------------------------
Unmapped points DFF E Total => E means Error node (TIE_E)
--------------------------------------------------------------------------------
Unreachable 106 34 140 => unreachable points are OK. Usually spare FF/latch in rtl are unreachable.
Not-mapped 8 0 8 => These Not-mapped points are not OK. These should be 0. Fix these before proceeding
================================================================================
Revised:
--------------------------------------------------------------------------------
Unmapped points Z Total
--------------------------------------------------------------------------------
Unreachable 7 7 => unreachable points are OK.
Not-mapped 0 0 => These Not-mapped points are OK. Usually there aren't any of these in revised. These may exist in eco designs, where o/p of some gates may not be used anymore in newer design, but there was no way to delete these.
================================================================================
For the "Not-mapped" points above, tool will try to remodel and map them, since w/o that mapping, key point mapping is incomplete and LEC can't proceed. Most of the times, tool is able to prove these are unreachable and moves them to "U" category.
report unmapped points -summary > reports/summary.rpt => displays list of unmapped poitns. to see if there are any unmapped points. Mapped points can also be reported by using "report mapped points"
report unmapped points -extra => OK to have these
report unmapped points -unreachable => OK to have these
report unmapped points -notmapped => NOT OK to have these in rtl.
add compared points -all => to specify which mapped points conformal compares. default is all. Only mapped points are compared.
compare => starts comparison. shows progression from 0 to 100%.
=> Out of all mapped points, compared points are reported for equiv/non-equiv.
// 5016 compared points added to compare list. => NOTE: not all mapped points (5231) got added to compare list. This is because some mapped points got merged/converted/remodeled to get better matching.
================================================================================
Compared points PO DFF DLAT BBOX Total
--------------------------------------------------------------------------------
Equivalent 609 3989 104 2 4704
--------------------------------------------------------------------------------
Abort 0 310 0 2 312 => If there are abort points, tool automatically tries harder until all "compared points" are done comparing.
================================================================================
report compare data -class nonequivalent -class abort -class notcompared >> reports/summary.rpt => view a list of all compare points and their status (equiv or non-equiv). When -class added, then only compare points belonging to that class are shown
#get_compare_points -diff -count => If this is anythnig > 0, then designs aren't equiv. This cmd can be used in tcl mode only.
#optional
#report_unmapped_points -golden -notype BBox > unmapped.golden.rpt
#report_unmapped_points -revised -notype BBox > unmapped.revised.rpt
#reporting floating nets is helpful to find out large current issues.
#report_floating_signals -golden -all > floating.golden.rpt
#report_floating_signals -revised -all > floating.revised.rpt
#below 5 cmds are helpful when we have non-eq points and we want lec to analyze and try again. works only with "-xl" license of lec.
#analyze noneq -verbose
#analyze setup -verbose
#add compare points -all
#compare
#report compare data -class nonequivalent -class abort -class notcompared >> reports/summary.rpt
report verification -verbose >> reports/summary.rpt=> reports a table of all violations as "non std ,modeling options used", "incomplete verifications", "design modifications", "extended checks" and "design ambiguity"
report statistics >> reports/summary.rpt => summarizes mapping and compare stats
exit => to exit tool
-------------
RC Compiler:
-----------
In RC compiler, we write dofile using this cmd:
write_do_lec -revised_design digtop.v -logfile rtl2final.lec.log > rtl2final.lec.do => tool assumes that design loaded into RC is RTL design. -revised_design specifies gate level netlist. If -golden_design is not specified, RTL design loaded with read_hdl cmd is considered golden and hier comp is done. If -golden_design is specified with gate level netlist, then flat comp done since both are gate level netlists.
NOTE: Even if we don't write out dofile explicitly, RC automatically generates one (after synthesize cmd is run) and puts it in fv/<DIGTOP>/rtl_to_g1.do. This has OVF directives useful for mapping. OVF file is also put in same dir. RC also generates dofile w/o OVF which is in fv/<DIGTOP>/rtl_to_g1_withoutovf.do
Above cmd generates rtl2final.lec.do file. It has following cmds:
0. general setup:
tclmode => prompt shows TCL_*>
vpxmode => prompt doesn't show TCL_ anymore. start entering conformal cmds.
#abort cmd in dofile specifies how to respond to errors. <on | off | exit>
set dofile abort exit => exits the session if any errors in dofile
usage -auto
#log file
set log file logs/rtl2final.lec.log -replace
#oovf file that does transformation for module ports,clk-gaters, etc.
vpx read guide file fv/S1/rtl_to_g1.ovf
set naming rule "_" "" -array_delimiter -golden
set naming rule "%s_reg" -register -golden
set naming rule %L.%s %L[%d].%s %s -instance
set undefined cell black_box -noascend -both => All referenced modules should either be defined or blackboxed. On finding an undefined cell, conformal exits. To prevent it from erroring out, blackbox undefined cells. It's always inserted by write_do_lec cmd. However, avoid this as it can mask a user error.
set undriven signal Z -golden => undriven signal is set to "z" for golden design in auto generated dofile. In RC, undriven signal can be set to 0,1,X,none(default). In LEC, the "none" default setting is translated to "Z" default setting.
1. Read library: It reads library in liberty format (since liberty files are used during synthesis). It can also read simulation library in verilog format, but only V-1995 format is supported.
read library -statetable -liberty -both \ => -ststetable and -liberty are always present in dofile gen by RC
/db/pdk/lbc7/rev1/diglib/msl270/r3.0.0/synopsys/src/MSL270_W_125_2.5_CORE.lib \
/db/pdk/lbc7/rev1/diglib/msl270/r3.0.0/synopsys/src/MSL270_W_125_2.5_CTS.lib
2. Read RTL design: Read rtl, elaborate and set top level to digtop. read_hdl in RC gets translated into read desgn
read design -rangeconstraint -configuration -vhdl 93 -golden -lastmod -noelab \
../../Source/spi_typedefs.vhd \
../../Source/spi.vhd
elaborate design -golden
set root module digtop -golden
3. Read Synthesized gate level design, and set top level to digtop :
read design -verilog -revised -lastmod -noelab netlist/digtop.v \
elaborate design -revised => sometimes, elaboration is not needed for gate level design
set root module digtop -revised
4. params/settings
set undefined cell -noascend black_box -both => this cmd always added by RC as it tells to make all undefined cells blackbox. This should NEVER be used in user gen dofile, as it can mask real errors for undefined cells.
report design data
report black box
//analyze and apply OVF Transformations loaded above by reading ovf file
vpx apply guided transformations
vpx report guide information
uniquify -all -nolib
set flatten model -seq_constant -seq_constant_x_to 0 => this added if any of the const 0 or 1 flops, or const latches are optimized in RC.
set flatten model -nodff_to_dlat_zero -nodff_to_dlat_feedback
// set parallel option -threads 4 -license xl
set analyze option -auto
#write out dofile based on all cmds above and then run that dofile. We do hier compare since then it's easy to debug which modules failed.
write hier_compare dofile outputs/hier_rtl2final.lec.do \
-noexact_pin_match -constraint -usage -replace -run_hier \
-prepend_string "analyze datapath -module -verbose; usage; analyze datapath -verbose"
#dofile generated above has cmds for comparing each module of design. Only modules that have same input/ouput pins for both revised/golden are considered for hier compariosn. also, modules which have <50 instances in them are skipped for hier comp, since they are easy to be compared at top level. Once hier comp is done for a module and it's equiv, it's blackboxed, and then blackbox model is used when doing hier comp for other module. This dofile has cmds which look like this:
1. comparing one of the sub-modules S1_CLOCK_GATE:
set system mode setup => setup mode
set root module S1_CLOCK_GATE -Golden
set root module S1_CLOCK_GATE -Revised
set module property -instance /I_S1_TIMER/I_S1_CLOCK_GATE -Golden
set module property -instance /I_S1_TIMER/I_S1_CLOCK_GATE -Revised
add pin equivalences XRESET FE_OFN42_xreset_r -hier -Revised => add pin equiv in revised since one pin can have multiple copies.
add ignored inputs I_PIN_YGPIO[5] -Golden => ignore certain i/p pins for golden.
report black box -NOHidden
set system mode lec => lec mode
analyze datapath -module -verbose; usage; analyze datapath -verbose => this string added doing write of dofile.
add compared points -all => adds all PO and state points to compare list
compare -noneq_stop 1 => compare stops on 1st non-equiv point
save hier_compare result
usage
2. blackbox the above module and compare next sub-module. If this sub-module instantiates other sub-modules, then they are blackboxed and compared.
set system mode setup
add black box S1_CONTROL_S2 -module -hier -Golden => blackbox above module
add black box S1_CONTROL_S2 -module -hier -Revised
set root module S1_CONTROL_HUNT -Golden => start with new sub-module
set root module S1_CONTROL_HUNT -Revised
...
3. comapre root module after comparing all sub modules. Root module will blackbox submodules that are directly instantiated in it.
set system mode setup
add black box S1_TIMER_WRAPPER -module -hier -Golden => blackbox the last submodule. All other submodules have been blackboxed.
add black box S1_TIMER_WRAPPER -module -hier -Revised
set root module digtop -Golden => set module to digtop
set root module ditop -Revised
set module property -instance / -Golden
set module property -instance / -Revised
...
save hier_compare result
usage
set system mode setup
report hier_compare result -usage
report hier_compare result -Non_equivalent -usage
report hier_compare result -Abort -usage
report hier_compare result -Uncompared -usage
--------------------
The dofile can be run using any of the 2 cmds below
1. run hier_compare outputs/hier_rtl2final.lec.do
2. dofile outputs/hier_rtl2final.lec.do
#report hier compare results
set system mode lec
tclmode
puts "No of diff points = [get_compare_points -diff -count]"
if {[get_compare_points -diff -count] > 0} {
puts "ERROR: Different Key Points detected"
}
vpxmode
exit -force => exits Conformal
--------------------------------
Running LEC for LINT checks:
------------------------
We can run lec for doing LINt checks by running lec in gui mode and doing read design on rtl, and then going to Tools->HDL Rule on gui to see all rule violations
home/kagrawal/> lec -gui -log lec.log -dofile check_rtl.do
NOTE: We can also just run "lec" and then from gui goto "Do Dofile" and select "check_rtl.do" file. This will run the script. Just be sure to do a "reset" before running dofile to load new results.
check_rtl.do has following:
-----------
set directive off synopsys
read library -verilog2k /db/pdkoa/lbc8lv/current/diglib/msl458/PAL/CORE/verilog/*.v /db/pdkoa/lbc8lv/current/diglib/msl458/PAL/CTS/verilog/*.v
set rule handling RTL14 -Ignore -library => ignore certain rules for library cells, as we want to see violations for our RTL code only
set rule handling VLG9.2 -Ignore -library
set rule handling UDP3.2 -Ignore -library
set rule handling DIR6.1 -Ignore -library
set rule handling DIR6.2 -Ignore -library
set rule handling IGN2.1 -Ignore -library
set rule handling IGN3.2 -Ignore -library
set rule handling HRC3.16 -Ignore -library
set rule handling HRC3.10a -Ignore -library
set rule handling RTL1.1 -Ignore -Design -Golden => to ignore certain rules for design (design can be -Golden or -Revised or Both)
read design ../../rtl/meson_clock_gate.v \
../../rtl/i2c_top.v \
-Verilog2k -sv -Golden -sensitive -root i2c_top
NOTE: on changing the RTL, we can rerun the design from within gui window by running this on cmd line:
SETUP > reset
SETUP > dofile check_rtl.do
---------------------------------------