Formal Verification Example

Formality (from Synopsys) is the tool used to formally verify the design. The design SAMM is verified in two ways. Gate level netlist and testable netlist are formally verified. Gate level netlist in .db format is taken as reference and testable netlist in .db format is considered as implementation. The matching of these two netlists generates below log data:


*********************************** Matching Results ***********************************
498 Compare points matched by name
0 Compare points matched by signature analysis
0 Compare points matched by topology
27 Matched primary inputs, black-box outputs
0(1) Unmatched reference(implementation) compare points
0(2) Unmatched reference(implementation) primary inputs, black-box outputs
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Input ports (Port) 0 2
Output ports (Port) 0 1
****************************************************************************************


There are total two unmatched input ports exists in implementation. These ports are test_se and test_si which are related to Design for Test (DFT) scan circuit. Since under normal operation DFT circuits doesn’t come into picture tool has to be instructed not to match these ports. This is performed by setup option in Graphical User Interface (GUI) and setting those two signals as false as shown in below.

Formality (match)> setup
1
Formality (setup)> set_constant -type port i:/WORK/sam3/test_se 0
Set 'i:/WORK/sam3/test_se' to constant 0
1
Formality (setup)> set_constant -type port i:/WORK/sam3/test_si 0
Set 'i:/WORK/sam3/test_si' to constant 0
1



After setting these options designs match and verification succeeds. The log data of the same is shown below.


Status: Verifying...
********************************* Verification Results *********************************
Verification SUCCEEDED
----------------------
Reference design: r:/WORK/sam3
Implementation design: i:/WORK/sam3
480 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 31 449 0 480
Failing (not equivalent) 0 0 0 0 0 0 0 0
Not Compared
Constant reg 18 0 18
****************************************************************************************
1


Similarly original verilog code and testable netlist is verified.

Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques