Step 0: Start Formality
    linux/unix> fm_shell
    or you may want to start interactively
    linux/unix> fm_shell -gui

Step 1: You may want to set some variables:
set HOME /homes/amittal
set RTLHOME $env(RTLHOME)
set TARGET_TECH $env(TARGET_TECH)
set DESIGN SSF

Step 2: Setup DesignWare root. This is needed if your design have
design ware instantiated components.
       set hdlin_dwroot /homes/synopsys2006_06_SP2
Step 3: Set Variables
    (a). set the variable hdlin_warn_on_mismatch_message, so that
formality does not fall over warnings
        set hdlin_warn_on_mismatch_message "FMR_VHDL-1002 FMR_VHDL-1027 FMR_VHDL-1014 FMR_ELAB-146    FMR_ELAB-149 FMR_ELAB-130 FMR_ELAB-117 FMR_ELAB-034 FMR_ELAB-261"
   
    (b). Set verification_clock_gate_hold_mode. This variables identifies clock gates in your implemented design
       set verification_clock_gate_hold_mode any

    (c). Set verification_inversion_push : This variable will enable matching of registers  in the implementation design
    which have used QN output, to corresponding reference design registers, which will by default use something which
    is equal to Q output of a register.
    instead of Q.
       set verification_inversion_push true

    (d). Formality tries to match the objects in the reference to implementation, by using names. You may want to instruct
    formality of some 'rules' which you think will help formality to match names. Here are some variables associated with it
set name_match_filter_chars             "'~!@#$%^&*()_-+=|\[]{}':;<>?,./"
set name_match_use_filter               true
set name_match_allow_subset_match       false

    (e). Formality also uses 'signatures' to match ref compare points to impl. You may want to enable/disable it
set signature_analysis_match_compare_points true

    (f). While reading in a design, it may be possible that some of your design objects are not available, and still
    you would like to go ahead with the formal verification, to verify the rest of your design.
    You can set them as 'black_box', if you would like to. Setting them black box both in ref and implementation
    will disable verification of anything inside this black box. Here is how you do it
set hdlin_unresolved_modules black_box

    (g). Its clever to set the variable so that formality stops verification, after a few errors, or it will
    keep on running without serving any useful purpose. Say I want formality to stop verification
    after 10 failures, then:
set verification_failing_point_limit    10


Step 4: set setup file(svf file) path and name. This file is written by design compiler, which
contains all the transformations it has done as 'guide' commands for formality. This is a very
important file, and without it, its difficult to pass formality. You may have multiple svf files
for the same design, because if you synthesize a design A, and then instantiate it into another B,
then synthesize design B, it will write its own svf, and you will need this svf as well. You may
hand write your own svf as well. svf is a collection of 'gudie' mode commands.
set svf_path ${RTLHOME}/${DESIGN}/synopsys
SVFS {A.svf B.svf}
foreach x $SVFS {set_svf -append $svf_path/$x}
(b) : Design Compiler by default makes binary svfs. You may want to convert into txt file:
report_guidance -to svf.txt
From V 2005.09 onwards, formality writes a txt corresponding to binary svf by default when
'set_svf' command is issued. But this command is still useful because the contents of dwsvf
directory is not converted to ascii text by default.
Step 5. Read in your reference design files in container called 'r'
       read_vhdl -container r matrixing.vhdl
       read_vhdl -container r ssv.vhdl
       read_vhdl -container r mult_ssf.vhd

Step 6: Link your design: In this phase formality tries to elaborate your design and
tries to find you links to instantiated designs. If a design links successfully, go ahead,
if not, try to find out why.
set_top r:/WORK/${DESIGN}

Step 7: Read in your implemented design usually a netlist, in container called 'i'
       read_verilog -container i -netlist ${RTLHOME}/${DESIGN}/synopsys/verilog/${DESIGN}_scan.v
Setp 8: Link your implemented design:
       set_top i:/WORK/${DESIGN}
Step 9: Disable Scan/DFT logic
set_constant -type port r:/*/$DESIGN/ScanEnable         0
set_constant -type port i:/*/$DESIGN/ScanEnable         0
set_dont_verify_point r:/*/$DESIGN/*ScanOut[*]
set_dont_verify_point i:/*/$DESIGN/*ScanOut[*]

Step 10:  Match Reference and Implementation. It is important to match
                the two i.e ref and implementation before going to verify stage.
                If there are unexplained mismatched items in both impl and ref, its better to
                spend time on working on it, rather than to proceed to verify stage.
                Unexplained means excluding obvious mismatches such as clock gate
                latches.
match
    (b). Report unmatched objects for datapaths. This helps in detecting multipliers
    report_unmatched_points -datapath
Setp 11 : Verify and Write Reports and quit.
if [ verify r:/WORK/ARM926EJS i:/WORK/ARM926EJS ] {
        quit
} else {
        report_matched > matched_points.fm
        report_unmatched > unmatched_points.fm
        report_failing > failing.fm
        report_error_candidates > error_candidates.fm
        quit
}

BACK[Why Use Formality]                              NEXT[Some Example commands used on live projects(s)]

HOME