原创 Formality : Quick tutorial(copied)

 2008-10-10 15:00  10403 7 7 分类: FPGA/CPLD

copy from: http://www.vlsiip.com/formality/

Formality Introduction:

Formality is a
tool from Synopsys, which is used for Formal
Verification.

Formal
verification is a method to verify two designs without running

simulations that they are functionally
equivalent. Of course one design

is the 'reference'
design, which is supposed to be a 'good'
design, and

the second design which is called
implementation design, is what is

sought to
match the 'reference' design.

Usually
two
kinds of verification are common using formality

I would use
ref for reference and impl for implementation hence forth.

1. RTL(ref) vs
Netlist(impl)

2. Netlist vs
Netlist

Why Use Formality?

Ok, but why,
why do we have to use formal verification.

RTL vs Netlist
is used to verify that the synthesis has been ok, i.e the resulting

netlist is
functionally equal to the RTL. Well we can always simulate the netlist

to verify that
the netlist is ok, but netlist sims take time, they can run for hours

days, and in
some cases even weeks. Now suppose that after running days of

simulation,
you found a very small bug, you fix it in RTL, synthesize it, produce

netlist. Now
without the existence of any formal verification, you would run days

of simulation
again. With formal verification, you can quickly verify that the netlist

out of
synthesis is corresponding to what the RTL is, thus saving you lot of
time.

Netlist vs
Netlist is may done to verify

1. Pre layout
and Post layout netlists : After PnR, you produce a 'post layout'
netlist

To check if
this netlist is functionally equivalent to the 'pre layout nelitst',
formal verification

is a popular
choice.

2. eco
changes. Suppose you change a gate or

two for fixing
timing or for any other purpose. For example you insert a buffer to fix

a hold
violation in the netlist manually, you would then like to be sure that
nothing else

has broken as
a result. Again using formality, you can easily verify it, without it??
run

days long sims
again??

How to run Formality

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

}

Some Commands

Formality
Commands Used On Live Project(s)

set_constant -type
cell
{r:/WORK/a926ejsIBIU/CurrentAddr_reg[1]} 0

guide

guide_reg_constant
-design
ARM926EJS_WRAP
U1/uCORE/u9EJ/uARM9/uCORECTL/uIPIPE/uJDEC/NxtStateD_reg[7] 0

setup

The above commands sets the reference design register to a constant.
Note no 'r:' has been mentioned

read_verilog -container r -libname WORK
/homes/amittal/s5/hw/rtl/unit/arm/src/ARM926EJS_WRAP.v

set_top r:/WORK/ARM926EJS_WRAP

read_verilog
-libname WORK -netlist -c i
/homes/amittal/s5/hw/rtl/unit/arm/AT230-BU-00000-r0p5-01rel1/synopsys/build_dir/ARM926EJS_WRAP.v

set_top i:/WORK/ARM926EJS_WRAP

verify

report_black_box

report_passing

report_failing

report_matching

set
verification_clock_gate_hold_mode low : used in RTL vs Netlist
for specifing clock gating.

set
hdlin_enable_rtlc_vhdl true

set_constant i:/WORK/ARM926EJS_WRAP/ScanEnable 0 -type port

set_constant r:/WORK/ARM926EJS_WRAP/ScanEnable 0 -type port

set_dont_verify_point i:/*/ARM926EJS_WRAP/*ScanOut

set_dont_verify_point r:/*/ARM926EJS_WRAP/*ScanOut

set_reference_design r:/WORK/ARM926EJSCore

set_implementation_design i:/WORK/ARM926EJSCore

set_black_box i:/WORK/ARM_RAM_WRAPPER

set_black_box r:/WORK/ARM_RAM_WRAPPER

remove_black_box i:/WORK/ARM_RAM_WRAPPER

remove_black_box r:/WORK/ARM_RAM_WRAPPER

Log messages: Explanation

Formality

Log : Click on the underlined links below to more know about them

1.

*********************************** Matching

Results ***********************************

4328 Compare points matched by name

0 Compare points matched by signature analysis

0 Compare points matched by topology

876 Matched primary inputs, black-box outputs

0(345) Unmatched

reference(implementation) compare points

0(0) Unmatched reference(implementation)

primary inputs, black-box outputs

7562(0) Unmatched reference(implementation)

unread points

***********************************************************************************

2.

----------------------------------------------------------------------------------------

Matched

Compare Points     BBPin    Loop

BBNet     Cut    Port

DFF     LAT   TOTAL

----------------------------------------------------------------------------------------

Passing

(equivalent)

0       0

0       0     853

34       0     887

Failing

(not equivalent)       0

0       0

0       2     198

0     200

Unverified

0       0

0       0      79

4932       0    5011

Not

Compared

Don't verify

0       0

0       0      64

0       0      64

****************************************************************************************

写原创有奖励！2024面包板原创奖励正在进行中