## 'Formality' : Equivalent Check ( RTL-to-Netlist )
=> 'Formality' is related to 'Design Compiler'
** Referecne
☞ http://www.vlsiip.com/formality/howtorun.html
** Environment
~/formality > setenv ECRUN_HOM /app/SOL/ECRUN
~/formality > set path = ($($ECRUN_HOME/bin $path)
~/formality > ec_run -Is -64 -f SCRIPT_DIR/SCRIPT_FILE.tcl -v Tool_Version -nogui | &tee LOG_DIR/TOP_DESING_NAME.log
=> for simple usage, the script ':run_ec' can be made as below;
-------------
#!/bin/chs -f
setenv ECRUN_HOME /app/SOL/ECRUN
set path = ($ECRUN_HOME/bin \
$path)
ecrun -Is -64 -f scr/$1.tcl -v 1109sp4 -nogui |& tee log/$1.log
-------------
** Directory & File
~/formality/SVF_DIR > *.svf // The Formality guidance file, known as the automated setup file, from Design Compiler
~/formality/NETLIT_DIR > *.v // Netlist from Synthesis
~/formality/RTL_DIR > *.f // RTL file list used for Synthesis
~/formality/SCRIPT_DIR > *.tcl // Script for Formality
~/formality/LOG_DIR > // log files are stored
~/formality/formality_svf > // Binary format(*.svf) is translated into ASCII format
~/formality/FM_WORK > // Reference, Implemenation files are generated
< Structure of formality.tcl >
## User Configuration
set SVF_FILE_NAME TOP_DESIGN_MODULE_NAME
set SRC_FILE_NAME TOP_DESIGN_MODULE_NAME
set TOP_DESIGN_NAME TOP_DESIGN_MODULE_NAME
## User Defined Set up
## For Example
set synopsys_auto_setpu true
set hdlin_error_on_mismatch_message false
set hdlin_ignore_full_case false
set hdlin_ignore_parallel_case false
set hdlin_dy_array_bnd_check none
set name_match_net true
set name_match_pin_net true
set search_path [ concat $search_path $*_dir \ ]
## DW(Design Ware) root
set hdlin_dwroot "/appl/SOL/Synopsys_Version"
## The version should be same as the Desing Comiler used for the synthesis
## Gated Clock
set verification_clock_gate_hold_mode low
## Undriven nets and ports
set verification_set_undriven_signals binary:X
## Verification Efforts
set verification_effort_level high
## Read Library Files
read_db *.db
## Formality Guidance File
set_svf ~/formality/SVF_DIR/$SVF_FILE_NAME.svf
## Read Reference Design Files
read_verilog ~/formality/RTL_DIR/$SRC_FILE_NAME.f
set_top r:/WORK/$TOP_DESIGN_NAME
## Read Implementation Design Files
read_verilog ~/formality/NETLIST_DIR/$SRC_FILE_NAME.v
set_top i:/WORK/$TOP_DESIGN_NAME
## Set Constant for Test mode signals : e.g. SCAN_ENABLE
## Test mode signals added in post-net : applied only to 'i'
set_constant - type port r:/WORK/$TOP_DESIGN_NAME/SCAN_ENABLE 0 // For RTL
set_constant - type port i:/WORK/$TOP_DESIGN_NAME/SCAN_ENABLE 0 // For Netlist
## Match : Make the svf to be applied to the design
match
## The name of the 'regs' in the rejected reg_merging guidance are possibly to be changed
## Set up : Check the 'regs' whose names are changed
setup
## Set constraints
## e.g. 'coupled' for the rejected 'reg_merging'
source CONSTRAINT_FILE.tcl
## Usage : set_constraint coupled { *_reg } r:/work/MODULE_NAME
## Match : Make the constraints to be applied to the design ?
match
## Verify
verify
## Report Files for Formality Analisys
report_unmatched_points > ./LOG_DIR/*.rpt
report_failing_points > ./LOG_DIR/*.rpt
report_matched_points -status unread > ./LOG_DIR/*.rpt
report_black_box > ./LOG_DIR/*.rpt
report_loop > ./LOG_DIR/*.rpt
## Save Session
save_session -replace TOP_DESIGN_NAME_ec.ses
## Exit
exit
cf. If 'exit' is skipped in the script file, the formality stops as below, and other commands is to be executed step by step ;
fm_shell (*) > ...
< SVF guidance which affects the Formality fail >
- reg_merging , reg_duplication , reg_constant rejection
- Others guidance : quide_uniquify, guide_multiplier, guide_datapath ... -> sometimes they'll cause the verification to run very slowly
< Reg Merging Information >
- can be with 'reg_merging rejected' message checked inf formality.log
- More easier way ;
fm_shell (*) > report_svf_operation -status {rejected} -command {reg_merging}
cf. Pay attention to modify the reg's name according to the actual name as what has been changed by svf operations
< DC Register Merging Optimization Disalbed >
dc_shell > set_register_merging reg_list false
