Formal Verification
Formal Verification
2
Agenda
Introduction to Formal Assertion Based Verification
■ What is the problem statement?
■ Temporal Logics
● LTL and CTL
● PSL and SVA
■ Model Checking
● CTL Model Checking
● LTL Model Checking
■ Symbolic Model Checking
● BDD and SAT based techniques
■ Abstractions
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
3
Problem Statement
Problem Statement
■ Verify an RTL design satisfies its functional requirements
Traditional Solution – Logic Simulation
■ RTL design specified in HDLs
■ Requirements specified as test vectors
Limitations of Logic Simulation
■ Limited set of test vectors
■ Exercise only a small fraction of design
■ Leads to undetected bugs
Example – Floating point division bug in Pentium
■ 1012 test vectors
■ Cost $470 million
4
Alternative Solution – Formal ABV
Formal Assertion Based Verification
Mathematically reason about correctness of RTL design
Properties specified in some form of “Temporal Logic”
Properties
Formal
Assertion Does property hold
Based on the RTL design?
Verification
RTL design
Benefits
■ Does not require user to provide test vectors
■ Does exhaustive verification
5
Agenda
Introduction to Formal Assertion Based Verification
■ What is the problem statement?
■ Temporal Logics
● LTL and CTL
● PSL and SVA
■ Model Checking
● CTL Model Checking
● LTL Model Checking
■ Symbolic Model Checking
● BDD and SAT based techniques
■ Abstractions
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
6
Temporal Logics
Logic extended with the notion of time
Reason about propositions qualified in terms of time
7
Linear Temporal Logic (LTL)
Introduced by Pnueli in 1977
Propositional Logic + discrete time
Time is viewed as a single linear sequence of events
Properties specified over a single path
Temporal operators to represent discrete tim
■ p is a proposition – p should hold at current time
■ X p – p should hold at next time
■ F p – p should hold in the future
■ G p – p should hold globally
8
LTL Formulas
Xp
Fp
Gp
pUq
pWq
Time
9
LTL - Examples
Safety Properties - G ¬(Critical1 ∧ Critical2)
■ Something bad never happens
Liveness - F (Req1 ∨ Req2)
■ Something Good will eventually happen
Fairness - G (Req1 F Critical1)
■ If something is requested, it eventually gets scheduled
Strong Fairness - GF (Req1 ∧ ¬ Critical2) GF Critical1
■ If something is repeatedly requested, it repeatedly gets scheduled
10
Computation Tree Logic (CTL)
A form of Branching Time Temporal Logic
Introduced by Clarke and Emerson
Temporal Operators as in LTL
■ Xp
■ Fp
■ Gp
In addition, path operators
■ A – Over all paths
■ E – There exists a path
11
Computation Tree Logic
AF p - On all paths, the property holds in the future
12
Computation Tree Logic
13
CTL Examples
Safety Properties
■ AG ¬(Critical1 ∧ Critical2)
Fairness
■ AG (state1 EF (¬ state1))
■ Self deadlock check for state1
■ AGEF (resetState)
■ A powerful and useful resetability test
Strong fairness
■ Cannot be specified in CTL
14
Comparison between LTL and CTL
Expressibility
■ Neither is superior to the other
■ LTL - Strong fairness CTL - Deadlock
■ CTL* - Superset of both LTL and CTL
Verification Complexity
■ LTL - Exponential in size of formula
■ CTL – Linear in size of formula
Compositional Verification
■ LTL – Yes CTL – No
Amenable to Simulation
■ LTL – Yes CTL – No
Preference in the industry – LTL flavor
15
Comparison between LTL and CTL
LTL CTL
Expressibility
Strong Fairness Deadlock
(CTL* superset of LTL and CTL)
Verification Complexity
Exponential Linear
(in size of formula)
17
Overview of PSL
Boolean Expressions
■ HDL expressions Verilog xor VHDL How
■ PSL/Sugar functions: rose(), fell(), prev(), ... When
What
Temporal Operators
■ always, never, next, until, before, eventually, abort, ...
■ @ -> |-> |=> ; { } [* ] [= ] [-> ] && & | :
Verification Directives
■ assert, assume, restrict, cover, ...
Modeling Constructs
■ HDL statements used to model the environment
18
Invariants
Something that should never happen!
For example: An underflow should never occur
Verification
Directive
How Temporal
When Operator Boolean
What Expression
GntA
if if if if if if if if
then then
GntB
clk
20
Multi-Cycle Conditional Behavior
Example: A Grant is always followed by Busy
assert_busy_after_Gnt : assert
always (GntA OR GntB) -> next Busy @(rising_edge (clk)) ;
assert_busy_after_Gnt : assert property (@(posedge clk)
(GntA || GntB) |=> (Busy)) ;
Implication (->) and
‘next’ together
express multi-cycle
conditional
GntA behavior
if if
GntB then
if
then
GntA
GntB
clk
22
Compound Assertions
Example: If Request is followed by Grant, then next is Busy, and next is Done
GntA if if if if if if
then then
Busy Evaluation
&& next && next starts again in
each cycle,
Done overlapping
previous
evaluations
clk
23
Agenda
Introduction to Formal Assertion Based Verification
■ What is the problem statement?
■ Temporal Logics
● LTL and CTL
● PSL and SVA
■ Model Checking
● CTL Model Checking
● LTL Model Checking
■ Symbolic Model Checking
● BDD and SAT based techniques
■ Abstractions
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
24
Model Checking Properties Formal
Assertion
Does property hold
Based
on RTL?
Verification
RTL design
Properties
PSL/SVA
Model Does property hold
Checking on the RTL design?
Model Checking
■ Does the model satisfy the property?
■ Does not require any test vectors
■ Does exhaustive verification
How does Model Checking work?
x
x
x
Model Checking
x x
x
x
x
■ Requires no test vectors
x ■ Works on entire state
x
x
space
■ Breadth first search
p [0]
FSM Model
p [1]
r=1
r=0 r=0
0 1 2 3 CTL Property
r=1 EF (p = 2)
Start state
Starting from start state, can the counter eventually count upto 2
27
CTL Model Checking
Evaluate the CTL property on the model
■ Evaluate EF (p = 2) on the FSM
r=1
r=0 r=0
0 1 2 3
r=1
p [0]
p [1]
FSM Model
r=1
r=0
CTL Property
0
r=0
1 2 3 EF (p = 2)
r=1
29
CTL Model Checking on the buggy design
Evaluate the CTL property on the buggy model
■ Evaluate EF (p = 2) on the buggy FSM
r=1
Least fixed Point
r=0
r=0
0 1 2 2
r=1
Buchi Automata
■ Accepting state is visited infinitely often
31
ω-automata for design
r=1 r
t [1]
r=0 t [0]
r=0
0 1 2 3
r=1
(r=1,t≠0) (r=0,t≠1)
(t≠0)
(r=1,t=0) (t≠0)
(r=1,t≠0) (r=0,t≠2)
(r=0,t=1) (r=0,t=2)
(r=1,t=0) (t=0)
(t=0)
32
ω-automata for design
(r=1,t≠0) (r=0,t≠1)
(t≠0)
(r=1,t=0) (t≠0)
(r=1,t≠0) (r=0,t≠2)
(r=0,t=1) (r=0,t=2)
(r=1,t=0) (t=0)
(t=0)
t=2
*
■ (t ≠ 2) (t = 2) (true)
ω
■ …........................................ (t = 2) ……………………………..
L(P) – Set of all valid behaviors of the property
34
LTL Model Checking
LTL Model Checking is Language Containment
Design behaviors is a subset of property behaviors
L(D) ⊆ L(P) or L(D) ∩ L(P) = ∅
(r=1,t≠0) (r=0,t≠1)
(r=1,t=0)
(t≠0)
(t≠0)
Cross
(r=1,t≠0) (r=0,t≠2)
(r=0,t=1) (r=0,t=2)
Product
(r=1,t=0) (t=0) (t=0)
t≠2
Complement Empty Language?
t=2
35
LTL Model Checking on our Example
F (t = 2)
(r=1,t≠0) (r=0,t≠1)
(t≠0) t≠2
(r=1,t=0) (t≠0)
(r=1,t≠0) (r=0,t≠2)
t=2
(r=0,t=1) (r=0,t=2)
(r=1,t=0) (t=0)
(t=0)
Will obtain a CEX – (r=1, t=0)ω
Add a constraint – G (r = 0) or always(r == 0)
Constraints are used to model environment and limit behaviors
L(C) – Set of all behaviors of the constraint
Check L(C) ∩ L(D) ∩ L(P) = ∅. Property will pass
36
Complexity of Model Checking
CTL Model Checking
■ Evaluate property over the FSM structure
■ Notion of fixed point computation
■ Complexity is linear in the size of the formula
LTL Model Checking
■ Notion of ω-automata
■ Translate design and property to ω-automata
■ Then LTL model check is simply a graph problem
■ Complexity is exponential in the size of the formula
What problem remains? The State Explosion Problem
■ Complexity is linear in the number of states in design
■ Exponential in number of state bits in the design
37
Agenda
Introduction to Formal Assertion Based Verification
■ What is the problem statement?
■ Temporal Logics
● LTL and CTL
● PSL and SVA
■ Model Checking
● CTL Model Checking
● LTL Model Checking
■ Symbolic Model Checking
● BDD and SAT based techniques
■ Abstractions
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
38
Binary Decision Diagrams
a
b
c out Ordered Decision Tree
out
a
0 1
a b c out b b
0 1
0 0 0 0
0 0 1 1 c c c c
0 1 0 0 0 1
0 1 1 1
1 0 0 0 0 1 0 1 0 1 1 1
1 0 1 1
1 1 0 1
1 1 1 1
39
Binary Decision Diagrams
out
Reduced Order BDD (ROBDD)
Merge isomorphic nodes
a Remove redundant tests
b b
out
c c c c
a
0 1 0 1 0 1 1 1 b
0 1
40
BDD based Symbolic Model Checking
Build a symbolic FSM model using BDDs
Perform fixed point computation on the symbolic FSM
Determine if property holds or not on the symbolic FSM
Properties
PSL/SVA
Symbolic Does property hold
Model on the RTL design?
Checking
41
Symbolic Model Checking on our Example
r
r
p1
p0 n0
p0
p1 n1
r=1 n1 n1 n1
r=0 r=0 n0 n0
00 01 10 11
r=1
0 1
r=0 r=0
00 01 10 11
r=1
p1
n1 p1
p0
∃r ( 0
n0
1
AND n1 n1 n1
) = p0
1 0
n0 n0
0 1
43
BDD Based Model Checking
Benefits
■ All operations can be done symbolically
■ Avoids upfront state explosion of explicit FSM
However, not a magic solution
■ Size of BDD dependent on variable order
■ Example – for an n-bit adder
● Best order is linear, Worst is exponential
■ Finding the optimal order is a very hard problem
● NP-complete problem
44
SAT (Satisfiability) Problem
(¬a ∨ b) ∧ (¬b ∨ c ∨ d)
45
Transforming design into a SAT problem
Can the output of a design take value 1?
a g
b
c p
46
r
Bounded Model Checking
Unfold the circuit “k” times
p
r0 r1 r2 rk-1
p0
p1 p2 p3 … pk
p0
48
Agenda
Introduction to Formal Assertion Based Verification
■ What is the problem statement?
■ Temporal Logics
● LTL and CTL
● PSL and SVA
■ Model Checking
● CTL Model Checking
● LTL Model Checking
■ Symbolic Model Checking
● BDD and SAT based techniques
■ Abstractions
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
49
Abstraction
Throw away information that is not required for proof
Abstraction is key to scaling capacity of model checking
One of most important abstraction
■ “Localization" abstraction
■ Throws away information not relevant to the given property
G (p Xp)
Make g a pseudo-input
50
Abstraction and Refinement
51
Other Advanced Abstraction Techniques
Proof based Abstraction-Refinement
■ Combines SAT based BMC and BDD based model checking
■ Uses SAT based BMC to find a suitable abstraction
Interpolation
■ SAT based Unbounded Model Checking
■ Uses over-approximate reachability analysis
52
Industrial Formal ABV Tools
Various Commercial Tools
■ Cadence – Incisive Formal Verifier
■ Synopsys – Magellan
■ Mentor – 0-in
■ Jasper – JasperGold
■ OneSpin, Real-Intent, Averant, Axiom
Combination of Symbolic Model Checking and Abstractions
Can handle local properties
■ Typically can scale to around 10K state bits
Global properties are still difficult
■ Need advanced abstractions and compositional techniques
53
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
■ Methodology
● Planning for Formal Verification
● Property Coding Guidelines
● Formal Verification Flow
■ Case Studies
● Protocol Compliance : Bridge Validation
● Arbitration
● Interrupt Sorter
● Memory Controller
● SoC Connectivity
● SoC Performance
54
Need for Efficient Methodology
State explosion problem (insufficient resources) very real !
Abstraction is the key
■ Automatic
■ Manual
No golden abstraction(s) to solve state explosion problem
Analysis is important (apriori and dynamic)
■ For handling formal proof complexity
■ For predictability of FV usage and results
55
Reality Bites!
80% of medium / large sized modules experience state explosion
■ For one or more assertions
■ No golden abstraction(s) apply across all designs
70% of initial counter-examples are spurious
■ More so because of incorrect constraints, rather than incorrect
assertions
■ Decomposition in practical scenarios lacks formalism
50-70% of time is consumed in modeling / setup / coding
■ Rest is tool run time
56
Need for Verification Planning
Verification Objective: Close verification within a predicted schedule
■ Planning
● Complexity Estimation, Verification Plan, Partitioning and Abstractions
■ Execution
● Analyzing indeterminate results
● Adding / Removing / Optimizing Constraints
● Identification and Closure of False Failures
● Iterations could be large – due to adhoc constraint updates
■ Closure – Signoff
● Coverage analysis, Verification report
All the above are inter-related
■ Closure has no meaning if results are indeterminate
■ Indeterminate results point to lack of proper abstraction
■ Lack of proper abstraction results from improper planning
57
Formal Verification Decisions
Abstraction decision
■ Identify sweet spots (control versus data path)
■ What parts of the design need to be abstracted out?
Modeling decision
■ Choosing the correct way of modeling the property
■ Complex SERE’s versus simple properties
Property decision
■ Which language ? Which AIP’s ? Glue logic ?
Tool specific Decision
■ Chose the correct FV engine
■ Chose correct tool (abstraction) options
58
Formal Verification Planning
Predict the problems in advance
■ Based on design knowledge, tool, experience, etc
Predict
■ Approximate design complexity (design analysis)
■ Approximate proof complexity (related to constraints and logic cone of
assertions)
Decide
■ Whether to partition or not ? Where to partition ?
■ Abstraction mechanism associated with the partitioning
■ How to code assertions / constraints properly?
■ What engines / methods to use for what scenarios?
59
Planning Step-I: Identify the sweet spots
Sweet spots : Control logic verification
■ Bus Bridges , Arbitration Logic
■ Controllers (FSM logic, Memory Cntlr, Interrupt Cntlr)
■ Control dominated Logic (Stall, Pipeline …)
Not so sweet spots
■ Complex Serial Protocols
■ Modules with large FIFO’s
■ Protocol interfaces with huge latency parameters
Negative candidates : Datapath intensive blocks
■ Data Transformation Blocks (Filters …)
■ Blocks with complex arithmetic units (Multipliers, Adders)
60
Planning Step-II: Analyze the module
Identify the functionality of the block to be verified
Identify the functionality of the surrounding blocks.
■ Check for well defined interfaces (standard protocols)
Prepare detailed micro level bulleted English plan for
■ Assertions to be coded for block functionality
■ Constraints to be coded for functionality of surrounding blocks
■ Disable / Restrain any data-path interfaces (address-data bits)
61
Planning Step-III: Estimate Complexity
Estimate Complexity for FV
■ (a) Number of flops in the module (first-crude estimate)
■ (b) Number of flops in logic cone of each assertion (finer estimate)
■ (c) Number of flops inferred because of constraint coding (adds to
complexity)
Good Candidate : < M flops ( (b) + (c) )
? Not so good Candidate : M – N flops ( (b) + (c) )
⌧ Negative candidates : > N flops ( (b) + (c) )
M ~ 1000 , N ~ 3000 Partitioning,
Restrictions needed
62
Planning Step-IV: Partition if needed
Structural Partitioning
■ Partition a design into a set of functionally independent and spatially
disjoint components
Functional Partitioning
■ Partition the design functionality itself into mutually exclusive logical
partitions
63
Structural Partitioning
Golden Rules for partitioning
■ Identify the sub-modules (specs must be clear) which can be verified
separately
■ Identify the ‘simple / sparse’ interface at which to cut
■ Partition the design and code constraints at the cut-points
■ Verify each partition in isolation (apply assume-guarantee)
Coding Constraints at cut-point-interface
■ Localization of the verification process
■ Abstraction is needed to benefit from decomposition
■ Golden Rule: “If surrounding RTL is replaced with equivalent constraints
No gain!”
64
Functional Partitioning
Identify mutually exclusive functional partitions
■ Example: Different modes of operation
65
Assume–Guarantee Reasoning
Properties can be used as either assertions or assumptions
Assume guarantee reasoning
■ DUV is block A
● assert pA; assume pB pA
■ DUV is block B
● assert pB; assume pA
A B
pB
Using Protocol AIP’s
■ at master interface
● assume prop_slave* , assert prop_master*
■ at slave interface
● assume prop_master*, assert prop_slave*
66
Functional Assume–Guarantee
Properties can be coded in layers (bottom up fashion)
Properties in a layer assume validity of properties in below layers
Application:
■ Prove the correctness of lower level properties
■ Apply them as constraints thereafter to prove higher level properties
■ Example : Arbitration validation:
Base level property: “The grants are zero-one-hot”
Higher level property: “check the arbitration scheme”
67
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
■ Methodology
● Planning for Formal Verification
● Property Coding Guidelines
● Formal Verification Flow
■ Case Studies
● Protocol Compliance : Bridge Validation
● Arbitration
● Interrupt Sorter
● Memory Controller
● SoC Connectivity
● SoC Performance
68
Property Coding Guidelines
Golden Rules:
■ Monitor style vs generator style
● For verifying RTL, do not create another one
■ Atomic vs Expressive Sequential properties
● Expressiveness adds proof complexity
■ Separability of functional checks
● Verify unrelated functional aspects in isolation
● Code separate properties for individual I/O’s of module
● Reduce input state space via pin-constraints
● Prove partitioned spaces are mutually exclusive
■ Incremental Property specification and verification
● Build up layers of properties
● Usually simpler to prove properties separately
■ Avoid integers, counters
69
Property Coding Guidelines
Guidelines – try these templates for each property
■ Can it be written as “condition should/shouldn’t always happen”
■ Can it be written as
● prev_state (implies) current_state
■ Can it be written using ‘event bounded window’ – something happening
between two specified events
■ Can it be written without using number of clocks (i.e. counter)
Event1 Event2
Event1 Event2
P P P P
assert_frame assert_window 70
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
■ Methodology
● Planning for Formal Verification
● Property Coding Guidelines
● Formal Verification Flow
■ Case Studies
● Protocol Compliance : Bridge Validation
● Arbitration
● Interrupt Sorter
● Memory Controller
● SoC Connectivity
● SoC Performance
71
Formal Verification Steps
Verification Setup
■ Sanity checks
■ Cover points
■ Constraint selection (incremental constraint addition)
Formal Engine Selection
Managing subsequent verification setup changes
■ Use structural coverage metrics
● Branch coverage, Expression coverage
● FSM checks
72
Formal Engine Selection
Engines targeted towards
■ Bug Finding
■ Complete Proof
Selection depends upon
ATPG
■ Estimated Sequential Depth (user decision)
.
ble
ha
■ Design characteristics
ac
● More breadth than depth owing to
Re
SAT
concurrent FSM’s FV
● Large sequential depths owing to counters, serial
Hy
shift registers
br
id
rac t ion
Abst
73
Structural Coverage Metrics
Metrics point towards ‘unreachable’ parts of the design under the set of
applied constraints – validates the ‘sanity’ of the constraints
Various set of metrics supported by tools
■ Branch coverage (Dead code analysis)
■ FSM checks
■ Expression coverage
Point to over-constrained, restricted verification environment
Managing constraint addition / removal
■ For every major constraint change, coverage analysis must be done to
filter out constraint related problems
■ Compare with past data
74
Formal Verification Flow
Model +
Modify assumptions
Refine the model or assertions
Properties
Over Constrain
Decompose, Abstract,
Model Checker
76
Bug Hunting Example: Dealing with FIFO’s
Interesting points to check: Overflow/Underflow
■ If possible, “reduce FIFO depth / width”
■ Else light-weight simulation to “reach near corner points”
(a) Dynamic Simulation (c) ApplyFV from this
to Bring System to a state onwards
Known State
Rd ptr
77
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
■ Methodology
● Planning for Formal Verification
● Property Coding Guidelines
● Formal Verification Flow
■ Case Studies
● Protocol Compliance : Bridge Validation
● Arbitration
● Interrupt Sorter
● Memory Controller
● SoC Connectivity
● SoC Performance
78
Bridge : Verification Targets
Functional Coverage Points: Structural Coverage Points
■ Protocol Compliance ■ Dead Codes
■ Address Decoding ■ FSM state / transition
■ Data Integrity ■ Structural checks (Out of
■ Arbitration bounds, FIFO full / empty)
■ Performance / Latency
79
Parallel Protocols
Control Variables
■ Define state of transaction (Command, Burst, Response)
■ Define legal / illegal states (reachable / unreachable)
■ Define legal / illegal transitions between legal states
Qualifier Variables
■ Add extra information to transaction (Address, Data)
Every protocol can be decomposed into functional layers
■ Atomic Transactions: basic transactions like read / write
● Handshake mechanism: Something holds until something else happens
● Basic definition for start / end of request, response
■ Complex Transactions: adds extra sequential information
● e.g. to bind atomic transactions in a “Burst mode”
● Basic definition involves start / end of transaction ‘windows’
■ Ordering: remember history of pipelined events
■ Out of order execution: properties for inter-thread transitions
80
Serial Protocols
DATA & CONTROL shared on same transmission line
■ Difficult to separate
Data-frames are spaced over several clock-cycles
■ Requires “HISTORY” info: Detecting a pattern requires
“remembering” previous train of signals – needs an FSM
■ E.g. Whether a train of 10 bits is a pre-amble or a post-amble
depends on the first 3 bits in that sequence.
Parallelism
Semantic (threads, Semantic
Information
Layer bursts) Layer
Assertions in a particular
level depends on those
at a lower level 82
AXI-OCP Bridge
Characteristics:
■ 1 AXI interface, 3 OCP-2.0 1 OCP
Interfaces AXI AXI-OCP
■ Flop Count : 560 Bridge 2 OCP
■ Pipeline depth (AXI) : 5 3 OCP
■ Threads Supported
■ Functional reset happens 2
Other Signals
cycles after reset is asserted
Scope of FV: Modeling:
■ Protocol compliance check ■ Divide & Conquer
■ No data integrity checks ● Verify each AXI-OCP path in
isolation
Initialization: Use Simulation
● Use Addresses to restrict
■ 2 cycles IDLE after primary reset
other paths
is asserted
83
AXI-OCP Bridge
Verification:
■ AIPs used for AXI and AXI 1 OCP
AXI-OCP
OCP Assume:
Master 2
Properties Bridge
■ First prove each path is 3
Assume:
Slave
independent Properties
always IDLE”
Handling indeterminate proofs:
■ Apply assume-
guarantee ■ Reduce pipeline depth, # threads
■ Prove assertions in ■ Prove each burst type separately,
bottom-up fashion using pin constraints
■ Bug hunting: initialization via
simulation
84
AXI-OCP Bridge
Project Statistics:
■ Number of Assertions : 125
■ Number of Constraints : 60
■ Number of Restrictions : 15
■ Total Time : 3 weeks (Tool runtime: 35%)
Sample Results
■ BUGS / Anomalies
● “Data was presented on the OCP port even prior to the corresponding
command acceptance on AXI”
● “Sequence of generated addresses incorrect for incrementing bursts”
85
I2C Controller [Gorai et al, DAC-2006]
OCP I2C
OCP1
OCP
Arbiter
OCP4
90
OCP Arbiter
Challenges
■Due to decoding logic, the proof complexity is very high
●Address constraints: Allow only some number of active slaves
●Restrict accesses: Take a set of 3 masters at a time
●Using proved properties as constraints
■Pipelining creates problems for accurate arbitration checks
●Need to keep external history for pipeline: External buffer keeps track of
‘number of pending requests’ counter implementation
91
Interrupt Controller [Biswas et al, CDNLive-2005]
Characteristics:
■ Sorting between 32/48/96 interrupts (configurable)
■ Mask and Priority configurable for each interrupt
■ OCP Interface (for configuration)
■ Flop Count : 785 (for 32 interrupts)
■ Output after 8 clock cycles (sorting in groups of 4)
Scope of FV:
Disabled
■ Protocol compliance check
■ Sorting Algorithm Verification Interrupts Sorting
Sorting winner
Algorithm
Algorithm
OCP
0 1 1 0
Prop_s
i
92
Interrupt Controller
Challenges
■ Mask & priority registers programmable via OCP interface
● Many combinations possible
Solutions:
■ Prove integrity of OCP data writes to internal registers
■ Then apply stability constraints on register
■ For intra-class checks, tie-off other interrupts
■ For inter-class checks, constrain values within each class to be same
■ Compare expected winner (computed by Verilog function) with actual
winner
93
Memory Controller
Characteristics:
■ Interface to SARAM core
■ Handshaking (with stall) with other bank-controllers
■ Total number of request buses (cpu, dma etc.) :9
■ Fixed Intra as well inter priority between requests
■ Pipelined CPU requests, DMA burst requests
■ Flop Count : 3500
■ Embedded SARAM, BIST controller
Scope of FV: Serialization check
● “Order of grants must be same as the requests”
● End-to-end property, encompasses all behavior of controller (mux, stall,
arbitration, etc.)
94
Memory Controller
SARAM
SARAMchannel
channel
SARAM Cores
Arbitration logic Strobe & inputs Output Stall Signals
Serialization
Stall behavior
95
Memory Controller
Solutions: White-box and Controlled Verification
■ Allow access to each core
● But intelligently disable parts/bits of address bus
■ Keep out other bank controllers
● Assume a floating primary input signaling their stall behavior
■ Identify and code assertions for internal points
● E.g. Code and prove assertions for stall module
■ Then use them as constraints
Results:
■ More than 30 bugs found, most of them corner cases (related to flush
functionality of pending buffers and stall behavior, which in turn lead to
serialization assertion failures)
■ Effort:
● Assertions : 215, Constraints : 12
● Total Time : 8 weeks (Tool runtime: 50%)
96
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
■ Methodology
● Planning for Formal Verification
● Property Coding Guidelines
● Formal Verification Flow
■ Case Studies
● Protocol Compliance : Bridge Validation
● Arbitration
● Interrupt Sorter
● Memory Controller
● SoC Connectivity
● SoC Performance
97
SoC Connectivity Verification
Bus Architecture Connectivity, I/O Pin-Muxing Logic
Errors caught easily and upfront in the design
■ Traditional verification involves exercising the complete communication
protocol from one end point to find any bug
■ Verification starts much earlier, issues get resolved quicker
■ Errors detected: tieoffs, unconnected points, wrong connections
Connectivity Description:
■ Interface Definition: Port, direction, width, high/low, etc.
■ Connectivity table: IPx-Porty to IPa-Portb
Results:
■ Properties: ~ 5000 (at top-level of a 5M gate chip)
■ Time: 6 hours
■ Note: not checking for validity of xls itself, nor IP functionality
To be done: Interrupt and Clock-reset connectivities
98
SoC Connectivity Verification
Track 1
PSL
RTL
Formal
Manual / Automated
Verification
Flow Generates RTL
Track 2
Connectivity related
bugs found
99
SoC Bandwidth Verification [Bhatia et al, DAC-2007]
Display Unit
Camera I/F
DMA
■ Multiple masters accessing the
Engine
JPEG
memory subsystem Memory
Traffic
■ Master starvation affects system Controller
performance
Interconnect
■ Traditional methods: simulation,
FGPA / emulation, running real
software on real silicon ARM Bridge
ISP
■ Formal Verification needed for
Graphics I/F
corner case analysis on real
RTL – early enough to fix design High Speed
AFE
Serial Port
bottlenecks
Properties:
■ Rate, e.g. "Requests are produced every ‘n’ time units": t(Request[i+1]) - t(Request[i]) = n
■ Latency, e.g. "Response is generated no more than ‘k’ time units after Request":
t(Response[i]) - t(Request[i]) <= k
■ Throughput, e.g. "at least ‘W’ Request events will be produced in any period of ‘T’ time units":
t(Request[i+W]) - t(Request[i]) <= T
100
SoC Bandwidth Verification
SEL
MIF
EMIF
Master 3
Master 4
101
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
Verification Closure: Coverage Analysis & Integration with Simulation
102
POWER5 Chip: It’s Ugly
POWER architecture:
Symmetric multithreading
Out-of-order dispatch and execution
Various address translation modes
Virtualization support
Weakly ordered memory coherency
103
Moore’s Law: AND It’s Getting Uglier
Complexity increases for POWER5, POWER6,
POWER7, …
Increase in speed
■ Contributes significantly to HDL
complexity
■ CEC methodology requires 1:1 latch
correspondence between circuit, HDL
● CEC=Combinational Equiv Checking
104
Complexities of High-End Processors
CEC methodology forces HDL to acquire circuit characteristics
■ Word-level operations, isomorphisms broken by self-test logic
● Self-test logic: much more intricate than mere scan chains
● Reused for functional obligations: initialization, reliability, …
105
Complexities of High-End Processors
CEC methodology forces HDL to acquire circuit characteristics
■ Timing demands require a high degree of pipelining
● And multi-phase latching schemes
106
Complexities of High-End Processors
Numerous techniques have been proposed for Processor Verification
107
Complexities of High-End Processors
Difficult to find places to attempt such abstractions on
high-end designs
■ Word-level info lost on highly-optimized, pipelined, bit-sliced designs
● Designs are tuned to the extent that they are “almost wrong” R. Kaivola
■ Time-consuming + error-prone to manually abstract the implementation
108
Complexities of High-End Processors
Industrially, “Formal Processor Verification” refers to proc components
■ E.g., verification of FPU, Cache Controller, Branch Logic
109
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
110
Reducing Verification Complexity
We discussed characteristics of high-end processors that make them
large, complex, difficult to verify
■ High degree of pipelining
■ Multi-phase latching schemes
■ Addition of sequential redundancy
■ Loss of word-level and isomorphic characteristics
111
Semi-Formal Verification (SFV)
SFV: hybrid between simulation and FV
■ Uses resource-bounded formal algos to amplify simulation results
■ Uses simulation to get deep into state space
112
Pipelining
High-end designs often use aggressive pipelining to break
computations across multiple clock periods
■ Increases #state elements; diameter
Min-area peripheral retiming may be used to drop latch count
■ Used as an automatic, property-preserving transform
“Transformation-Based Verification using Generalized Retiming” CAV01
113
Multi-Phase Latching Schemes
High-end designs often use multi-phase level-sensitive latches to better distribute
propagation delays vs. edge-sensitive flops
■ Increases #state elements; diameter
Phase abstraction can automatically convert multi-phase to simple-delay model
■ Unfold next-state functions modulo 2, removing oscillator + ~1/2 latches
114
Sequential Redundancy
High-end designs use sequential redundancy to minimize propagation delays
Pervasive logic sequential, yet disabled, logic intertwined with all latches
■ Increases #state elements; breaks isomorphisms, word-level properties
Numerous techniques exist to identify, merge redundant gates
“Exploiting Suspected Redundancy without Proving It” DAC05
115
Reducing Complexity through Transforms
High-end design complexities can be (partially) alleviated through
automated transformations and abstractions
116
Transformation-Based Verification
Counterexample
Design +
Trace consistent with
Properties
Original Design
50000 registers
Redundancy SixthSense
Problem Removal
Redundancy-
decomposition Engine
removed
via synergistic
40000 registers trace
transforms All transformations
are transparent to the user
Localization
Redundancy-
Engine
All results are in terms removed,
of original design localized trace
150 registers
Reachability
Engine
117
Reducing Verification Complexity
Automated techniques are continually increasing in capacity
However, for complex proofs, manual techniques are critical to push the
capacity barrier
■ Choice of testbench boundaries
■ Manual abstractions to reduce design complexity
■ Underapproximations and overapproximations
■ Strategic development of constraints and properties
The best strategy often depends upon some knowledge of available algos
118
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
119
Processor Verification Concepts
A verification Testbench comprises
■ Design components under verification
■ Input assumptions
● May be represented as constraints
● Or may be overridden by random drivers
We refer to either scheme as a driver
■ Properties to be checked
● Coverage metrics, assertions, equivalence vs. ref model
■ Initialization information
● Initial states impact reachable states which impacts pass vs fail
120
Processor Verification Concepts
Verifying a proc component is basically the same as verifying any design
■ However, due to high-performance logic, verifying architectural
properties typically requires a Testbench which is too large for proofs
Options:
1. Develop unit-level Testbench without worrying about proof feasibility
2. Develop minimal Testbench encompassing only functionality to be
verified
121
Processor Verification Concepts
1. Develop unit-level Testbench without worrying about proof feasibility
■ Unit-level testbenches often built for sim regardless
● Use of synthesizable language reusable for FV, emulation, …
123
Basic CPU Architecture
Load-
Store
Unit (LSU)
Floating
Instr Instr Point Global
Fetch Decode Unit (FPU) Completion
Unit Unit Fixed- Unit
(IFU) (IDU) Point (GCU)
Unit (FXU)
Branch
Execution
Unit (BXU)
124
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
125
Pseudo Case-Study: SEC
Performance-critical designs undergo many functionality-preserving
transforms
■ Timing optimizations
■ Power optimizations
■ Addition of test and run-time monitoring logic
Inputs =?
Initialized
NEW Design
126
Pseudo Case-Study: SEC
Due to synthesis limitations, transforms often done manually
■ Entail risk of (late) error introduction
■ Suboptimalities tolerated to minimize error risk
127
Pseudo Case-Study: SEC
SEC also useful for:
■ Reference-model style verification
● Less circuit-like model serves as extensive “property set”
128
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
129
Instruction Dispatch Case Study
Concerns the portion of the Instruction Decode Unit responsible for
routing valid instruction groups to execution units
Flushes / Rejects
Instructions
Instructions
Instr Instructions
Fetch Instr
Staging Instr
Unit Dispatch To
+ Decoded Logic Buffer Logic Execution
Decoder ICache Units
Line
Stall
130
Instruction Dispatch: Verification Goals
Verify that Dispatched instructions follow program order, despite:
■ Stalls
■ Flushes (which roll back the Dispatch flow to prior Instr Tag)
■ Branch Mispredicts (similar to Flushes)
■ Rejects (which force re-issue of instructions)
■ Bypass path
131
Instruction Dispatch: Logic Boundaries
First choice: what logic to include in Testbench?
■ Independent verif of Instr Buffer, Staging Logic, Dispatch Logic attractive
from size perspective, but hard to express desired properties
● Decided to include these all in a single testbench
132
Instruction Dispatch: Input Modeling
Second choice: how to model input behavior
■ Needed to carefully model certain instruction bits to denote type
● Branch vs. Regular types
133
Instruction Dispatch: Property Modeling
Third choice: how to specify properties to be checked
■ Dispatches follow instruction order:
● Easy check since driver uses bits of instr to specify program order
● Check for incrementing of these bits at Dispatch
134
Instruction Dispatch: Proof Complexity
Recall that driver tricks were used to entail simpler properties
■ Check for incrementing “program counter” bits in Dispatched instr
Shortcut possible since this logic treated most instruction bits as data
■ If Testbench included execution units, shortcut would not be possible
135
Instruction Dispatch: Proof Complexity
Philosophy: “don’t be precise where unnecessary for a given testbench”
is very powerful for enabling proofs
■ Instr Dispatch requires precise Instr Tag modeling due to flushes; does
not care about decoded instr
■ Some downstream Execution Units don’t care about Instr Tag; require
precise instr code
136
Instruction Dispatch: Proof Complexity
Semi-Formal Verification was main work-horse in this verification effort
■ Wrung out dozens of bugs
● Corner-cases due to Flushes, Stalls, Bypass, …
137
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
138
Instruction Fetch Case Study
Motivated by an encountered deadlock:
■ Instruction Fetch Unit stopped fetching instructions!
InitFetch
Instr’s
Fetch
Instr.
Instr
Fetch Instr
State ICache Buffer
Machine
Branch To
Instr
Execution Execution
Pipeline
Unit Units
139
Fetch-Hang Case Study
Suspected: Instr Fetch State Machine (IFSM) can enter illegal hang state
■ Discovered a hang state – yet could not readily extrapolate the tiny
counterexample to one of the entire IFU+IDU
● Exhibited input timings thought to be illegal
● Yet designer was able to discern a scenario which, if producible, could lead
to deadlock
140
Fetch-Hang Case Study
Given extrapolated scenario, next attempted to produce that scenario on
larger IFU+IDU components
■ Interfaces at this level were very easy to drive
● Abstracted the ICache to contain a small program
141
Fetch-Hang Case Study
Extrapolated scenario:
■ Stream A is being executed, encounters a branch to B (to be taken)
■ Instructions in-line from A are still being fetched to Instr Buffer at
time of branch resolution
■ Somehow the in-line instructions are not immediately invalidated
■ Fetch to B is delayed until exactly the point that the in-line
instructions are dispatched out of the Instr Buffer (InitFetch)
● This can put the IFSM into the dangerous hang state
■ Somehow a Mispredict Flush does not get triggered (to squash the
in-line instructions) to break IFSM out of the hang state
time
142
Fetch-Hang Case Study
Reachability of hang state on full Testbench possible with BMC
■ However, normal execution always kicked IFSM out of hang state
time
144
Fetch-Hang Case Study
Built a protocol-style model of entire system, merely comprising timing
information and handling of relevant operations
145
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
146
FPU Case Study
Floating point number format: M * BE
■ M: Mantissa e.g. 3.14159
■ B: Base, here B=2
■ E: Exponent, represented relative to predefined bias
● Actual exponent value = bias + E
Guard bits, rounding modes, sticky bits used to control rounding errors 147
FPU Case Study
Highly-reusable methodology developed for FPU verification
148
FPU “Numerical Correctness”
Uses a simple IEEE-compliant reference FPU in HDL
■ Uses high-level HDL constructs: + - loops to count number of zeros
■ Imp: 15000 lines VHDL; Ref-FPU: <700 lines
164 bit
2e_addend 2e_prod
mantissa addend ..00
mantissa product …00
+/- a+b
cnt leading 0’s copy and round
Leading zero’s can happen, e.g.,
1.101011
– 1.101001
S Exp Frac Final IEEE result = 0.000010
149
FPU Complexity Issues
Certain portions of FPU intractable for formal methods
■ E.g., alignment-shifter, multiplier
■ Case-splitting
● Restrict operands each subproblem solved very fast
● Utilize batch runs subproblems verified in parallel
150
FPU Case-Splitting
Four distinct cases distinguished in Ref-FPU
■ Based on difference between product, addend exponent
δ = e prod − ec where e prod ( = ea + eb − bias ) is the product exponent
and ec is the addend exponent
C δ := ( e a + eb − bias = ec + δ )
152
FPU Normalization Shift Case-splits
Normalization shifter is used to yield a normal result
■ Depends upon # number of leading zeros of intermediate result
153
FPU Results
Development of methodology required nontrivial trial-and-error to ensure
tractability of each proof
■ And some tool tuning…
154
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
■ Complexities of High-End Processors
■ Algorithmic Methods for Reducing Verification Complexity
■ Processor Verification Case Studies
● Sequential Equivalence Checking (SEC)
● Instruction Dispatch Case Study
● Instruction Fetch-Hang Case Study
● Floating-Point Unit Verification
● Load-Store Verification
155
Load-Store Unit Case Study
Numerous properties to check of LSU and Memory Infrastructure:
■ Multiprocessor cache coherency properly maintained
■ Correctness of associativity policy
■ Proper address-data correlation and content maintained
■ Parity and data errors properly reported
■ Data prefetching stays within proper page limits
■…
156
Cache Coherence Case Study
Cache coherence protocol requires masters to obtain a clean snoop
response before initiating a write
■ Obtain Exclusive snoop to write, clean snoop to read
■ Otherwise data consistency will break down
Mandatory for driver to adhere to protocol, else will spuriously break logic
Other tricks:
■ Parameterize RAM! Caches often are VERY large
■ Can limit # addresses that can be written to, but need to take care that
exercise sectoring, N-way associativity, …
158
Associativity Case Study
N-way associative caches may map M>N addresses to N locations
■ When loading N+1’th address, need to cast a line out
■ Victim line often chosen using Least-Recently Used (LRU) algo
Verify: newly-accessed entry not cast out until every other entry accessed
160
Address-Data Consistency
Drive data as a function of addr
■ Validate that outgoing addr-data pairs adhere to encoded rule
■ Should trap any improper association and staging of data
Drive poisoned data values if known that they should not be transmitted 161
Parity / Error Detection Correctness
Error code schemes are based upon algorithms:
■ Properly diagnose <I bit error code errors, <J data bit errors
■ Properly correct <K bit data errors
162
Prefetch Correctness
Prefetch logic is a performance-enhancing feature
■ Guess addresses likely to be accessed; pull into cache before needed
■ Often use a dynamic scheme of detecting access sequences:
● Start by fetching one cache line
● If continued accesses to prefetched stream, start fetching multiple lines
163
Prefetch Correctness
Generation of illegal prefetch addresses checkstop
■ Most prefetching is required not to cross address barriers
● E.g. must be done to same page as actually-accessed addr
■ Can restrict address stream being generated, or monitor addr stream,
and validate that prefetch requests stay within same page
Also wish to verify that prefetch initiates prefetches when it should, does
not when it shouldn’t
■ Often done using a reference model or set of properties to encode
specific prefetching algorithm
164
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
165
Design Intent Verification
Design
Design Intent
Intent Design
Verification
Specification
Specification
Design
Design
Implementation
Implementation
Design
Design Intent
Intent
Modeling
Modeling
Design Intent
Verification
166
What is design intent verification?
Design Intent
■ A set of abstract high-level global safety and liveness requirements
Design Intent Modeling
■ Developing a set of high-level component models that mimic the
expected behavior of the components
Design Intent Verification
■ The models taken together should satisfy the design intent
167
Traditional: Without intent verification
Comp
Comp--11 Comp
Comp--11
Specs
Specs Design
Design
Comp
Comp--22 Comp
Comp--22
Design Specs
Specs Design
Design
Design Intent
Intent Specs
Specs Integrated
Integrated
(English)
(English) Design
Design
Comp
Comp--kk Comp
Comp--kk
Specs
Specs Design
Design
Sub - system
Design of
Tech. Specs
the parts
(English)
Design Verification
168
Emerging: With intent verification
Comp
Comp--11 Comp
Comp--11
Specs
Specs Design
Design
Design
DesignIntent
IntentSpecs
Specs Integrated
Integrated
(English)
(English) Design
Design
Comp
Comp--kk Comp
Comp--kk
Specs
Specs Design
Design
Sub - system
Design of
Tech. Specs
the parts
(English)
Comp
Comp--11 Verif.
Design F--Model
Specs
Design Intent
Intent of the
(Formal Specs)
(Formal Specs) parts
Comp
Comp--kk
F--Model
Specs
Sub -system Integrated
Design Intent Design
Models
Verification
- Verification
Can be done before implementation
169
Intent Verification – Everywhere?
Digital design verification
■ Micro-architectural properties (SVA / PSL)
■ RTL properties (SVA / PSL), RTL blocks
Mixed-signal design verification
■ Integrated power mgmt chips (LDOs, buck converters, battery charger)
■ Modeling options include VerilogA, VerilogAMS
Embedded systems
■ Safety critical properties
■ Modeling options include Matlab, UML statecharts
170
Design Intent Verification – Why?
Practical considerations
■ Components are out-sourced, and integrated into the design at the end
(sometimes as black-boxes)
Helps in developing the component specs before implementation
Helps in developing acceptance tests for the components and verifying
the integrated design
171
Dimensions
Discrete Models
Continuous Models
Boolean Logic
Hybrid Models System
Temporal Logic
Type Formal FSM
specs Equations
Satisfiability
Core Hybrid Automata
Synthesizability Problems
Formal coverage
Model Checking
172
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
173
Verification is all about coverage
Valid Invalid
Implementation
Implementation
174
Verification as coverage
Implementation
Implementation
If:
• R is a function that captures exactly the set of all behaviors
of the given implementation, and
• A is the specification,
Then the verification problem is to check for the validity of R ⇒ A
A bug is a witness for R ∧¬A
175
Verification Methodologies
A bug is a trace that acts as a witness for R ∧¬A
176
Compositional Verification & Coverage
A: Specification
Properties
Verification
M1 M2 Mk
R : Implementation
177
Two key problems
A: Specification
What should be our approach when R
Properties consists of state machines for some
components, properties for some
Verification components and executable black
boxes for the rest?
M1 M2 Mk
R : Implementation
178
Model checking as coverage analysis
Sample property: If the counter is not reset, then the next value of
the counter differs from the present value by exactly one bit.
179
Model checking as coverage analysis
180
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
181
Priority Cache Access
G[ r1 V r2 ⇒ XX[ d1 V X( ¬d2 U d1 ) ] ]
183
One possible architecture
G[ r1 V r2 ⇒ XX[ d1
V X( ¬d2 U d1 )]]
184
Developing block specs
Target:
A1: G[ r1 V r2 ⇒ XX[ d1
V X( ¬d2 U d1 )]]
Arbiter:
R1: G[ r1 V r2 ⇔ Xa ]
R2: G[ z3 V z4 ⇔ Xb ]
185
Design Intent Coverage
Arch. Specs:
A1: G[ r1 V r2 ⇒ XX[ d1
V X( ¬d2 U d1 )]]
RTL Specs:
R1: G[ r1 V r2 ⇔ Xa ]
R2: G[ z3 V z4 ⇔ Xb ]
R3: G[ a ⇒ X[ w U d1 ]]
R4: G[ ¬b ⇒ ¬X d2 ]
R5: G[ r3 ∧ ¬w ⇔ z3 ]
Is it possible to have an implementation R6: G[ r4 ∧ ¬w ⇔ z4 ]
that satisfies R1, …, R6, but refutes A1?
186
In this case, we have a gap!!
Target:
A1: G[ r1 V r2 ⇒ XX[ d1
V X( ¬d2 U d1 )]]
Arbiter:
R1: G[ r1 V r2 ⇔ Xa ]
R2: G[ r3 V r4 ⇔ Xb ]
188
Intent Coverage Problem: Formally…
Given:
■ Architectural specification A, consisting of a set of temporal
properties over a set APA of Boolean signals
■ RTL specification R, consisting of a set of temporal properties
over a set APR of Boolean signals, such that
APA ⊆ APR
189
Specification Refinement
A: G( (¬r2 ) ⇒ X g1)
R: G( (r1 ∧ ¬ r2) ⇒ X g1 )
(a) G( r1 ∨ r2 ∨ X g1 )
(b) G( ( ¬X g1 ∧ ¬r1 ) ⇒ r2 )
(c) G( (¬ r1 ∧ ¬r2 ) ⇒ X g1 )
(c) is visually closest to A – our goal is to show the coverage gap as (c).
190
Spec. Refinement by Relaxation
191
The SpecMatcher Tool
System-level
Design refinement
Spec. refinement
Intent
Coverage
Block-level
test plans
Intent
Coverage
Dynamic ABV
Simulation +
Unit level specs
A: Specification Advantages:
• Scalable
Properties • Can be done top down, before implementation
Verification Disadvantages:
• Requires more user involvement
M1 M2 Mk
R : Properties for M1 … Mk
A: Specification
Pure Design Intent Coverage
Properties
Verification
Advantages:
• Less user involvement M1 M2 Mk
Disadvantages:
• Capacity limitations
R : State m/c for M1 … Mk
Pure Model Checking
194
Between Intent Coverage and Model Checking
A: Specification
Properties Approach-1:
•Find the gap, T, between A and
Verification
the properties of Mi+1 … Mk
M1 M2 Mk •Model check T on M1 … Mi
[Source: Das et. al. What lies between Design Intent Coverage and
Model Checking? DATE 2006]
195
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
196
Consistency and Completeness
Verification: R ⇒ A
Consistency issues:
■ Verification is vacuous when R is unsatisfiable
■ Verification is vacuous when A is valid
Completeness issues:
■ Verification closure depends on the completeness of A – have I
written enough properties?
197
Formal Consistency Analysis – Why?
Are my properties correct?
■ Debugging formal specifications can be quite hard
■ Coding errors – new languages, alien semantics
■ Logical errors
Am I checking the right property on the right design?
■ A typical BUS protocol consists of:
● Properties over individual components: master, slave, arbiter
● Global properties
■ In the absence of proper assume constraints, checking global properties
on individual components can lead to realizability problems.
Reasoning about formal specifications
■ Logical implication
■ Coverage analysis
198
Verification is Logical Consistency
Verification is mostly about checking logical implication
Model checking:
■ Does the product of the component state machines logically imply each
of the formal properties?
Design intent coverage:
■ Do the properties of the component modules together imply the
architectural properties of the design?
Logical implication ≡ Satisfiability / Validity
199
Unsatisfiable Specification
When the master is not in the IDLE or WAIT states, the request line, req, should be
kept high
The master lowers the request line, req, sometime
property ReqHighDuringTransfer;
@ (posedge clk)
(state != ‘IDLE || state != ‘WAIT) |-> req ;
endproperty
property ReqIsSometimesLow;
@ (posedge clk)
##[0:$] !req ;
endproperty
200
The Correct Specification
When the master is not in the IDLE or WAIT states, the request line, req, should be
kept high
The master lowers the request line, req, sometime
property ReqHighDuringTransfer;
@ (posedge clk)
(state != ‘IDLE && state != ‘WAIT) |-> req ;
endproperty
property ReqIsSometimesLow;
@ (posedge clk)
##[0:$] !req ;
endproperty
201
Vacuity
When the gnt signal is high, the master should not be in the IDLE or WAIT
states
property UseBusWhenGranted;
@ (posedge clk)
gnt |-> (state != ‘IDLE || state != ‘WAIT) ;
endproperty
202
Realizability of Open System Specs
Whenever the high-priority request, hreq, arrives, the grant, hgnt, is given for
one cycle
property HighPriorityGrant ;
hreq hgnt
@ (posedge clk) Arbiter
hreq |-> ##1 hgnt ##1 !hgnt ;
endproperty
203
Realizability = Satisfiability ∀ Inputs?
Not quite. Consider the following properties:
■ Each request is eventually granted
■ The request line is lowered one cycle after the grant
property Gnt ;
@ (posedge clk)
req |-> ##[1:$] gnt ; req gnt
Arbiter
endproperty
property LowReqAfterGnt ;
@ (posedge clk)
gnt |-> ##1 !req ;
endproperty
204
Receptiveness
property LowReqAfterGnt ;
req gnt
@ (posedge clk) Arbiter
gnt |-> ##1 !req ;
endproperty
205
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
206
Have I written enough properties?
Paradox:
■ If I had a formal definition of the coverage goal, then that itself could become the
formal specification!!
Solution:
■ Evaluate the formal property specification with some structural coverage metric
■ The structural coverage metric should be such that:
● Low coverage indicates gaps in the specification, and I need more
properties
● High coverage does not necessarily mean that I have enough properties
207
Types of Coverage Approaches
Mutation-based Approaches
■ A given implementation is used as the reference
Fault-based Approaches
■ A given fault model is used as the reference
Design Intent Coverage
■ A higher level specification is used as the reference
208
Mutation-based Coverage
Specification:
00 State: (g1,g2) P1: g1 is never asserted in consecutive cycles
property NoConsecutiveG1;
@ (posedge clk) g1 |-> ##1 !g1 ;
10 01
endproperty
Abstract FSM of a P2: g2 is never asserted in consecutive cycles
Round-robin Arbiter
Approaches:
Falsity coverage: Mutate the FSM and check whether the truth of
any property changes.
Vacuity coverage: Mutate the FSM and check whether any property
becomes vacuous.
209
Mutation-based Falsity Coverage
s0 Specification:
00 State: (g1,g2)
P1: g1 is never asserted in consecutive cycles
s1 s2 P2: g2 is never asserted in consecutive cycles
10 01
Abstract FSM of a
Round-robin Arbiter
s0 P1 fails.
s0
10 00
⇒ The value of g1 at s0 is covered
s1 s2 s1 s2
10 01 P2 fails. 11 01
⇒ The value of g2 at s1 is covered
Mutant-1 Mutant-2
(g1 flipped at s0) (g2 flipped at s1)
210
Mutation-based Vacuity Coverage
Specification:
s0
00 State: (g1,g2) P1: g1 is never asserted in consecutive cycles
property NoConsecutiveG1;
s1 s2
@ (posedge clk) g1 |-> ##1 !g1 ;
10 01 endproperty
Abstract FSM of a P2: g2 is never asserted in consecutive cycles
Round-robin Arbiter
Falsity coverage
s0 No property fails.
00 ⇒ The value of g1 at s1 is not covered
s1 s2
00 01 Vacuity coverage
P1 is satisfied vacuously.
Mutant-3 ⇒ The value of g1 at s1 is covered
(g1 flipped at s1)
211
What does mutation coverage mean?
If mutations on many parts of the implementation do not affect the truth
of the properties, then it is likely that our specification does not cover
those behaviors that are exhibited by those parts of the implementation
■ Extensions to transition coverage, path coverage, etc
■ Extensions to simulation coverage metrics, such as code coverage
(mutations on the HDL code) and circuit coverage (toggle coverage on
latches and signals)
Does this mean that 100% coverage ⇒ we have written enough
properties?
212
High Coverage is not good enough
00 01 00 01
10 11 10 11
Property P: The next value of the counter differs from the present
value in exactly one bit (100% state coverage, but …)
[Source: A Roadmap for Formal Property Verification, Springer, 2006] 213
Fault-based Coverage Analysis
Core Idea: Inject a fault into the specification and test whether the
specification remains satisfiable / realizable
Fault Model
■ Stuck-at faults on one or more signals
■ Possible counter-example scenarios
Good for a first-cut check on the first formal specification
■ Low coverage means we need more properties
■ High coverage does not necessarily mean we have sufficient properties
214
Stuck-at Fault Coverage
Output Fault Coverage:
■ A stuck-at fault on a non-input y is covered if there exists some scenario
where the specification forces y to take the opposite value
Input Fault Coverage:
■ A stuck-at fault on a input x is covered if we cannot realize the
specification without reading that input x
215
Example: Output Fault Coverage
Memory arbiter: mem-arbiter(input r1, r2 ; output g1, g2)
r1 g1
Priority of g1: G ((r1 ∧ r2) X g1)
Arbiter g2
r2
Mutex: G (¬g1 ∨ ¬g2)
g2 s-a-0 is not covered – we can have a valid implementation that never asserts g2 !!
216
Example: Input Fault Coverage
Memory arbiter: mem-arbiter(input r1, r2 ; output g1, g2)
g1
Priority of g1: G ((r1 ∧ r2) X g1) r1
218
The Integrated Flow (Recap)
System-level
Design refinement
Spec. refinement
Intent
Coverage
Block-level
test plans
Intent
Coverage
Dynamic ABV
Simulation +
Unit level specs
220
The notion of context
Two types of properties:
■ Invariants – properties that must hold always
● Example: An arbiter must never assert two grants at the same time (mutex)
■ Context sensitive properties
● Example: In a burst mode transfer, addresses wrap around the 2KB
address boundaries
221
Assertion Coverage
Assertion coverage attempts to determine whether the simulation has
covered scenarios where the assertion was checked non-vacuously
■ How do we check the vacuity?
■ Many definitions:
● Implication vacuity
● Explicit specification of coverage goals – such as cover properties in SVA
● Gaming definitions
222
Implication vacuity
Property: If the request r is asserted, then the grant g must be asserted
in the next two cycles, unless r is lowered in between.
property P;
@ (posedge clk)
r |-> ##1 (g or (!g && !r) or ((!g && r) ##1 g) ;
endproperty
If r is asserted and the DUT does not assert g in the next cycle, then we
should drive r again to check the remaining part of the property
■ Otherwise, the real intent of the property is not checked
223
Property-driven test generation?
It’s a game …
Two types of games – same players, but the winning conditions are different
■ Vacuity games
■ Realizability games
[Ref: Banerjee, et.al., DAC 2006]
224
Vacuity Games
In any round of the game, the inputs written by Player-1 (TB) is vacuous iff P
is satisfied under these inputs regardless of the values of the outputs in that
round
■ Player-1 (Test bench)
● It loses if in any round it writes vacuous inputs
● It wins if in any round it writes non-vacuous inputs and yet the
property is satisfied or refuted
■ Player-2 (DUT) loses when Player-1 wins, and wins when Player-1
loses
The values written in a round re-defines the property for the next round
225
Realizability Games
Problem with unreceptive specifications
■ In some round of the game, the property for the next round may become
unrealizable, but satisfiable
■ This means that Player-1 (TB) has a winning strategy from that round – if it uses
that strategy then the property for some future round will become unsatisfiable
226
Example – tic-tac-toe
X ? X X : Environment
0 : DUT
0 X
? 0
227
Integration into Test Environment
Assertion
Assertion Monitor
Monitor
++
Game
Game Oracle
Oracle
Test
Test
DUT
DUT Bench
Bench
228
Agenda
Introduction to Formal Verification
Case Studies from TI: Protocol & Control Logic Verification
Case Studies from IBM: Formal Processor Verification
Verification Closure: Coverage Analysis & Integration with Simulation
■ Design Intent Verification
■ Verification as Coverage Analysis
■ Design Intent Coverage and Specification Refinement
■ Reasoning about Specifications
■ Have I Written Enough Properties?
■ Property Directed Simulation Games
■ The Integrated Picture
229
The Design Intent Verification Flow
Design Intent
(Formal Properties) Test
Generator Integrated
+ Design
Uncovered behaviors
Assertion
Monitor
Coverage
Analyzer
Simulation + DPV Platform
4. Chockler, H., O.Kupferman, M.Y.Vardi, Coverage metrics for temporal logic model
checking. TACAS 2001, LNCS 2031.
232