Transcript Document
I NTRODUCTION TO V ERIFICATION
by Daniel Gomez Prado
ECE667 UMASS 09
Based on the slides for ECE667 at UMASS taught by prof. Ciesielski
The book “Verification techniques for system level design” by Masahiro Fujita 2008,
The book “SAT Based scalable formal verification solutions” by Malay Ganai 2007.
1
I NTRODUCTION
2
V ERIFICATION
3
Design verification = ensuring correctness of the design
against its implementation (at different levels)
against alternative design (at the same level)
=?
model
Design 1
Design 2
=?
behavior
=?
function
HDL / RTL
RTL
Logic level
Logic level
=?
structure
=?
Gate level
Gate level
Mask level
Mask level
=?
layout
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
=?
W HY V ERIFICATION
4
Verification crisis
System complexity, difficult to manage
More time, effort devoted to verification (70%) than to design
Need automated verification methods, integration
Consequences
Disasters, life threatening situations
Inconvenience (Pentium bug … ?)
Many more …
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
V ERIFICATION M ETHODS
5
Functional Simulation: performed on the model
Emulation, prototyping: product + environment
Testing: performed on the actual product
(manufacturing test)
Formal Methods
Deductive verification
Model checking
Equivalence checking
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
F UNCTIONAL V ERIFICATION
6
S IMULATION - BASED : VALIDATION
7
Goal: verify the design in the full operational context
RTL functional verification
Verify specification (HDL) of RTL model
No model to check against: must simulate
Functional simulation
Functional test generation
Automatically generate tests:
high-level transactions on data, clocking, control
SAT based methods
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
E VALUATING T EST C OVERAGE
8
Coverage metrics - facilities to measure the effectiveness of
functional verification
Monitors: collect data about testing (coverage, profile)
Code coverage
Functional verification coverage
low-level coverage statistics for states, transitions, HDL model line
coverage
statistics, monitors for events, state transition sequences (transactions)
data sets
Self-checking tests
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
F UNCTIONAL T EST G ENERATION
9
Given an RTL design and a coverage metric, must reach the
predefined coverage goal
Solution: run functional simulation
Directed tests
manual, often easy to generate (e.g. instruction set)
reliable (predictable coverage), but
not efficient (cover small portion of design)
Random tests
efficient (fast), but not reliable (unpredictable coverage)
Deterministic tests
Automatically generated
Constraints (user-defined, environment, coverage metrics)
Challenging to compute
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
10
F UNCTIONAL V ERIFICATION -
TYPICAL SCENARIO
100 %
Deterministic tests
?
Coverage
95 %
Pseudo-random directed tests
(reliable and efficient)
100.0
Normalized
verification
test cycles
1.0
50 %
Manual directed tests
(reliable, not efficient)
Test development time
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
FUNCTIONAL VERIFICATION
(DETERMINISTIC METHODS)
11
D ETERMINISTIC METHODS
12
SAT-based methods
Boolean satisfiability
BDD
Symbolic simulation
ATPG-based methods
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
B OOLEAN S ATISFABILITY (SAT)
13
Well known constraint satisfaction Problem.
Given a propositional formula Ψ, determine if there
exist a variable assignment such as Ψ evaluates to true.
If exist, Ψ is called satisfiable
If not, Ψ is called unsatifiable
SAT problems are NP complete
Most SAT solvers uses Conjunctive Normal Form (CNF)
to represent the propositional formula
Conjunction of clauses
Each clause is a disjunction of literals
DPLL A LGORITHM
14
David Putnam Logemann-Loveland (DPLL) procedure
Most used algorithm for SAT solver
A branch and bound search over the space of possible
Boolean assignments
Preprocessing, might find if it is unsatisfiable
Choose an un-assigned variable and assign a
value that has not been previously assigned
previous-level();
Implication Graphs
Boolean Constraint Propagation (BCP) to find
if there is a conflict in the assignment, that is
x=1 && x=0
Used by Modern SAT solvers to perform:
conflict driven learning
conflict driver backtracking
SAT: I MPLICATION GRAPHS
15
Node X1 means X1 = 1
This implies on C1 that X6 = 1
Node X2 means X2 = 0
1
0
0
0
0
0
0
0
1
1
1
1
0 0
0 0
0
1
1
1
1
=1
1
1
1
1
=1
SAT: B INARY D ECISION D IAGRAMS
16
Boolean logic +
constraints
Add constraints (modify the logic)
Build BDDs for each output, subject to constraints
Build the product BDD (AND of all BDDs)
If the set is empty, infeasible SAT instance
Otherwise: set of all satisfying assignments, test.
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
17
B INARY D ECISION D IAGRAM (BDD)
BDDs represent a Boolean function as an acyclic graph
BDD
Reduced
Ordered
BDD
ROBDD
Other variations:
Zero suppressed BDD (ZBDD)
Multivalue Decision Diagrams (MDD)
At its core implemented through BDDs
ROBDD is by far the
most used decision
algorithm in EDA!!
A BDD-SAT
18
EXAMPLE
• Given: output value requirements for a circuit
• Compute: satisfying assignments at the inputs
0
a
b
c
0
d
1
0
• Output requirements: u=1, v=1, w=1
• SAT assignments: a,b,c,d = ?
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
u
1
1
v
1
1
w
1
0
BDD-SAT EXAMPLE
19
Boolean satisfiability analysis
H
H = product BDD
a
set of all satisfying solutions
to test for H = 1 (0), find a path in the
BDD to terminal 1 (0)
the path, expressed in function
variables, gives a satisfying solution
(test vector)
{1,1,-},
ECE 667 - SYNTHESIS & VERIFICATION - LECTURE 22
{1,0,1}
b
ab
c
0
ab’c
1
A UTOMATIC T EST PATTERN G ENERATION
20
ATPG generates a suite of test vectors for testing a
manufactured circuit for manufacturing faults
All faults are assume to be modeled by stuck-at 0 or 1 fault
Incorporate sophisticated heuristic for Boolean reasoning
Only one fault at a time is considered
D-Algorithm
Path Oriented DEcision Making (PODEM)
FAN oriented decision making (FAN)
ATPG N EMESIS
21
All ATPG tools are sophisticated heuristics
Pros:
Fast for the circuits for which the heuristic was developed
Cons:
Not universal, they can’t find solutions for all circuits,
eventually a nemesis ckt will appear, for which the ATPG
approach proves to be poor.
F ORMAL V ERIFICATION
22
F ORMAL V ERIFICATION
23
Quick facts:
Mathematical analysis of proving or disproving correctness of
hardware respect to certain unambiguous properties
It provides 100% coverage respect to the properties is able to
prove
If it something can’t be proved a counter example is obtained
Do not require any test bench
Complements simulation
Two main classifications
Theorem proving
Model checking
T HEOREM P ROVING |D EDUCTIVE R EASONING
24
Create a mathematical proof for a given theorem, interactively:
A Theory and a proof system,
Formula whose validity must be proved
Its reasoning is:
Expressive, highly abstracted and powerful
Very difficult to automate, require user guidance for
parameters of the reasoning tool, such as:
Variable ordering, Induction hints, ordering of lemmas, etc
Require a “theorem prover guru” with substantial expertise on
the system under verification
Only used for critical applications
No guarantees that it will terminate
M ODEL C HECKING
25
Can be automated, therefore it’s attractive to industry
Its classified in:
Equivalence Checking
A golden model is used as reference
Any deviation from the golden model is a defect
Property Checking
The desired properties are specified in formal logic,
Any model must be verified against this formal logic.
M ODEL C HECKING
26
Limited by the State Explosion problem
Number of states is exponential in number of states
elements
Based on state enumeration techniques, they can be
classified as:
Explicit -> uses a hash table to map every single state
Implicit or Symbolic -> use canonical or semi canonical data
structures to traverse the state space.
Can use BDD and SAT
E QUIVALENCE C HECKING
27
Sequential Equivalence Checking (SEC)
Latch matching Problem
Find a mapping of latches between 2 circuits
Incomplete methods, ATPG, group latches
Complete methods, produce theoretically a mapping (van Eijk)
Combinational Equivalence Checking
Combinational Equivalence Checking (CEC)
Exploit the notion of structural similarities
CEC
28
Find Potentially Equivalent Nodes (PEN)
29
T YPICAL CEC TOOL