1
Lectures
Formal verification of SoC designs
(targeting logic verification only)
Masahiro Fujita
VLSI Design and Education Center (VDEC)
University of Tokyo
[email protected]
2
Table of contents


Introduction to SoC verification (Lecture 1)
Backgrounds technology in formal verification: Methods for reasoning about mathematical
models (Lecture 2)



Basic formal verification techniques



Boolean function (Propositional logic)
 SAT (Satisfiability checker)
 BDD (Binary Decision Diagrams)
Use of first-order and higher-order logic
 Logic of uninterpreted functions with equality
 Theorem proving methods
Equivalence checking (Lecture 3)
 Combinational
 Sequential
Model (property) checking (Lecture 4)
 Explicit/implicit state based
 Bounded model checking
Real formal verification tools

Enhancing Formal Verification Capacity (Lecture 5)








Abstraction-refinement
Assume guarantee/Compositional Reasoning
Approximation
Symmetry reduction
Partial Order Reduction
Industrial and Research Tool Offerings
Semi-formal verification techniques (Lecture 6)
Advanced topics

System level formal verification (Lecture 7)
 Synchronization verification
 Equivalence checking for C programs
3
Lecture 1: Introduction to SoC verification

System-on-Chip (SOC) design
 Increase of design complexity
 Move to higher levels of abstraction
Level
Number of components
1E0
System level
1E2
1E3
RTL
Gate
1E4
1E5
1E6
Transistor
1E7
Accuracy
Algorithm
Abstraction
1E1
4
System-on-Chip (SoC) design


Specification to architecture and down to
implementation
Behavior (functional) to structure


System level: system specification to system
architecture
RT/IS level: component behavior to component
micro-architecture
µProcessor
Control
IF FSM
IP Netlist
IP
Comp.
Memory
Pipeline
RAM
State
PC
Interface
Interface
IR
Control
Bus
Interface
Processors
IPs
Memories
Busses
Interface
Memory
Registers
ALUs/FUs
Memories
Gates
State
Datapath
Mem
RF
IF FSM
Memory
State
ALU
Custom HW
Specification
+ constraints
System architecture
+ estimates
RTL/IS Implementation
+ results
5
Verification challenge
Simulation/Design Verification
51%
Design Creation
32%
Place & Route
32%
Post Layout Optimization
26%
Parasitic Extraction
17%
System on Chip
17%
Design Rule Checking
17%
Static Timing Analysis
16%
Synthesis
15%
Delay Calculation
13%
0% 10% 20% 30% 40% 50% 60%
Bottlenecks in Design Cycles:
Survey of 545 engineers by EETIMES 2000
6
System-level design & verification
System-level
RTL
Transistor level
Bugs fix time
3 minutes
delay
3 days
delay
3 weeks
delay
Cost due to the delay/late time-to-market
revenue loss
Remove as many bugs as possible in the earlier stages
Do not introduce new design errors when refining designs

Formal verification in system-level designs:
Property checking and equivalence checking
7
Design representation in higher level


Super state: Need multiple cycles for executions
Variables, functions: Boolean ⇒ Integer, Term rewriting
Op1
PS1
Op2
PS2
SFSMD model
Op4
a = 42;
while (a<100)
{ b = b + a;
if (b > 50)
c = c + d;
a = a + c;
}
PS3
Op1
S1
Op3
Op2
Op5
Op6
Op3
S2
Op4
S3
Op5
FSMD model
Op6
Establish
mapping
Control
circuits
Datapath
circuits
8
Verification methods: simulation/emulation

Simulation
Traditional, basic, and flexible technique
 Applicable at any design levels
 Difficulties in preparing “good” simulation
patterns

 Getting harder to cover corner cases

Emulation
Can handle software simultaneously
 Cost and time for preparation: not ignorable
 Corner case problems still remain

9
Why formal verification?

Traditional method
(testing &
simulation)

Formal Verification
Test
properties
Deadlock
...
Test
vectors
Design
Under
Test
Patterned
vectors

Cannot cover all
possible cases
Possibility of surviving
subtle (corner case)
bugs
True
or
False
Find
counter-example


System
Model
Test
results


Equivalent to simulating
all cases in simulation
No bug (according to the
property)
Property (model) checking
and Equivalence checking
10
Formal verification

“Prove” the correctness of designs




Possible mathematical models




Both design and spec must be represented with
mathematical models
Mathematical reasoning
Equivalent to “all cases” simulations
Boolean function (Propositional logic)
 How to represent and manipulate on
computers
First-order logic
 Need to represent “high level” designs
Higher-order logic
 Theorem proving = Interactive method
Front-end is also very important

Often, it determines the total performance of the
tools
Spec
Design
Front-end
tool
Mathematical
models
Verification
engines
11
Formal vs simulation based verification

Example:

Verification of Exclusive-OR circuits:
 z = ~x&y + x&~y ( ‘~’ means compliment)
b
x
G2
a
G4
G1
y
G3
c
z
12
Example: Formal vs simulation (Cont.)

Verification of Exclusive-OR circuit with
“simulation”
z and ~x&y+x&~y are equal for all four cases
 Need to simulate 2**N cases where N is #ins

x
y
0
0
1
1
0
1
0
1
z ~x&y+x&~y
0
1
1
0
0
1
1
0
b
x
a
y
z
c
13
Example: Formal vs simulation (Cont.)

Verification of Exclusive-OR circuit with
“formal verification”
b
z = ~b + ~c
x
b = ~x + ~a
a
c = ~a + ~y
a = ~x + ~y
z = ~b + ~c
y
c
= ~(~x + ~a) + ~(~a + ~y)
= a&x + a&y
= (~x + ~y)&x + (~x + ~y)&y
= x&~y + ~x&y
 Axiomatic and mathematical transformation of
expressions to reach the specification
 This is a mathematical proof !
z
RTL Simulation Semantics

D delay model





4 valued logic is usually used (0, 1, X, Z)


more complex logic possible e.g. std_logic_vector in VHDL
Blocking and Non-blocking assignments using syntax



each operation takes negligible time
operations are scheduled in terms of clock boundaries
explicitly specified delay may be used
functional simulation may be different from later stage timing
simulation
blocking assignments are sequentially executed
non blocking assignments are executed in parallel at end of a
clock boundary
Value Change Dump (VCD) file captures changes in
values of variables with time
Event-driven Simulation

Event: change in logic value at a node, at
a certain instant of time  (V,T)
 Event-driven: only considers active nodes


Performs both timing and functional
verification



Efficient
All nodes are visible
Glitches are detected
Most heavily used and well-suited for all
types of designs
Event-driven Simulation
1
1
0
0
a
c
D=2
1
1
1
e
D=1
b
0
0
3
4
6
d
1
0
5
e(4)=0
b(1)=1
d(5)=1
d(5)=1
c(3)=0
d(5)=1
d(5)=1
e(6)=1
Cycle-based Simulation

Take advantage of the fact that most digital
designs are largely synchronous
L
a
t
c
h
e
s
Boundary Node
Internal Node
L
a
t
c
h
e
s

Synchronous circuit: state elements change value on
active edge of clock
 Only boundary nodes are evaluated
 Compute steady-state response of the circuit

at each clock cycle at each boundary node
Simulation CAD Tools

Event-driven simulators

Synopsys VCS, Sirocco
 VCS is a fast Verilog simulator
 Sirocco is a VHDL simulator



Cadence NCSim (VHDL, Verilog, mixed)
Model Tech. Modelsim (VHDL, Verilog, mixed)
Cycle-based simulators



Quickturn SpeedSim (VHDL)
Synopsys PureSpeed (Verilog)
Cadence Cobra
Debugging Tools

VCD dump viewer

e.g. Cadence Signalscan
clk
a
b
bus[0:3]
time

xxxx
0
10
5H
20
3H
30
40
50
Integrated debugging environment




more sophisticated tool
cross references code, VCD waveform viewer, coverage
analysis etc.
integrates software debug features and hardware debug
features
e.g. Novas Software Debussy
Lecture 2: Backgrounds technology in formal
verification

Methods for reasoning about
mathematical models
Boolean function (Propositional
logic)
 SAT (Satisfiability checker)
 BDD (Binary Decision Diagrams)
 First-order logic
 Logic of uninterpreted functions
with equality
 Higher-order logic
 Theorem proving = Interactive
method (skipped in this tutorial)
Spec
20
Design

Front-end
tool
Mathematical
models
Verification
engines
21
SAT Problem definition
Given a CNF formula, f :
(a,b,c)
A set of variables, V
 Conjunction of clauses
(C1,C2,C3)
 Each clause: disjunction of literals over V

Does there exist an assignment of Boolean values to
the variables, V which sets at least one literal in each
clause to ‘1’ ?
Example : (a  b  c)( a  c)( a  b  c)
C1
C2
C3
a=b=c=1
22
DPLL algorithm for SAT
[Davis, Putnam, Logemann, Loveland 1960,62]
Given : CNF formula f(v1,v2,..,vk) , and an
ordering function Next_Variable
Example :
0
(a  b)( a  c)( a  b)
C1
C2
C3
CONFLICT!
0
b
a
1 0
1
c
1
  
SAT!
C1
C3 C2
23
DPLL algorithm: Unit clause rule
Rule: Assign to true any single literal clauses.
(a  b  c)
=
=
c=1
0 0
Apply Iteratively: Boolean Constraint Propagation (BCP)
a(a  c)( b  c)( a  b  c)( c  e)( d  e)( c  d  e)
c(b  c)( c  e)( d  e)( c  d  e)
e( d  e )
24
Anatomy of a modern SAT solver
DPLL Algorithm
Clause database
management
Discard
useless
clauses (e.g. inactive
or large clauses)
Efficient BCP
Search Restarts
SAT
Solver
To
correct for bad
choices in variable
ordering
Restart
algorithm
“periodically”
Efficient garbage
collection

Retain
some/all
recorded clauses
Conflict-driven
learning
25
Conflict driven search pruning (GRASP)
Silva & Sakallah ‘95
x1
 Non-chronological backtracking
 Conflict-clause recording
x2
2
xj
SAT
xk-1
xk
1

26
Conflict analysis: An example
Current Assignment:
{x9  0 @1, x10  0 @ 3, x11  0 @ 3, x12  1@ 2, x13  1@ 2}
Decision Assignment:
{x1  1@ 6}
   ( x1  x 2)
 2  ( x1  x 3  x 9)
 3  ( x 2  x 3  x 4)
 4  ( x 4  x 5  x10)
 5  ( x 4  x 6  x11)
 6  ( x 5  x 6)
 7  ( x1  x 7  x12)
 8  ( x1  x8)
 9  ( x 7  x8  x13)
27
Example continued: Implication graph
x2= 1@6
1
x1= 1@6
2
2
3
3
x3= 1@6
x9= 0@1
x10= 0@3
4
4
x5= 1@6
6
x4= 1@6
5
6
5

x6= 1@6
x11= 0@3
c(   ( x1  x 9  x10  x11)
28
Example continued….
x9= 0@1
x8= 1@6
8
9
x1= 0@6
x10= 0@3
x11= 0@3
7
7
x12= 1@2
`
9
Decision
Level
9
3
x13= 1@2
5
x7= 1@6
x1
6
29
Variable ordering
 Significantly
impacts size of search
tree
 Ordering schemes can be static or
dymamic
 Conventional wisdom (pre-chaff):
Satisfy most number of clauses OR
 Maximize BCP
 e.g. DLIS, MOMs, BOHMs etc.

30
Variable ordering: New ideas

New wisdom: Recorded clauses key in
guiding search
 Conflict-driven variable ordering:



Semi-static in nature, for efficiency


Chaff (DAC’01): Pick var. appearing in most
number of recent conflict clauses
BerkMin (DATE’02): Pick var. involved in most
number of recent conflicts
Statistics updated on each conflict
Side-effect: Better cache behavior
31
Efficient Boolean Constraint Propagation


Observation: BCP almost 80% of compute time,
under clause recording
Traditional implementation:



Each clause: Counter for #literals set to false
Assgn. to variable ‘x’: Update all clauses having x, x
New Idea: Only need to monitor event when # free
literals in a clause goes from 2 to 1

Need to watch only 2 literals per clause : SATO
(Zhang’97),Chaff (DAC’01)
x1 … w1
…
w2 … xk
32
SAT solvers today

Capacity:



Formulas upto a million variables and 3-4 million
clauses can be solved in few hours
Only for structured instances e.g. derived from
real-world circuits & systems
Tool offerings:

Public domain





GRASP : Univ. of Michigan
SATO: Univ. of Iowa
zChaff: Princeton University
BerkMin: Cadence Berkeley Labs.
Commercial
 PROVER: Prover Technologies
33
Binary Decision Diagram: Decision structures
Truth Table
x1 x2 x3
0
0
0
0
1
1
1
1
0
0
1
1
0
0
1
1




0
1
0
1
0
1
0
1
Decision Tree
x1
f
0
0
0
1
0
1
0
1
x2
x3
0
x2
x3
0
0
x3
1
0
x3
1
0
1
Vertex represents decision
Follow green (dashed) line for value 0
Follow red (solid) line for value 1
Function value determined by leaf value
Source: Prof. Randal Bryant
34
Variable ordering

Assign arbitrary total ordering to variables


e.g. x1 < x2 < x3
Variables must appear in ascending order along all
paths
Not OK
OK
x1
x1

x1
x2
x2
x3
x3
x3
x1
x1
Properties


No conflicting variable assignments along path
Simplifies manipulation
35
Reducing OBDDs: Rule #1
Eliminate duplicate terminals
1
1
1
x1
x1
x2
x3
0
x2
x3
0
0
x2
x3
1
0
x3
1
0
x3
1
x2
x3
0
x3
x3
1
36
Reducing OBDDs: Rule #2
Merge isomorphic nodes, i.e. nodes that reference the same
variable and point to the same successors
a
0
1 0
a
a
1
b
c
0
b
x1
x2
x3
0
c
x1
x2
x3
1
x3
x3
1
x2
x2
x3
x3
0
1
37
Reducing OBDDs: Rule #3
Eliminate a node if its 0 and 1 edges lead to the same node
a
0
1
b
0
b
0
1
1
x1
x1
x2
x2
x3
x3
0
1
x2
x3
0
1
38
Example OBDD
Reduced Graph
Initial Graph
x1
x1
x2
x3
0

0
0
x2
x2
x3
x3
1
0
x3
x3
1
(x1 +x2 )· x3
0
1
0
1
Canonical representation of Boolean function


For given variable ordering
Two functions equivalent if and only if graphs
isomorphic
 Can be tested in linear time

Desirable property: simplest form is canonical.
39
From circuits to BDD
X1
G2
G4
G1
X2
G3
X1
0
1
1
X2
0
0
X1
X1
1
0
X2
1
1
1
0
1
0
X2
0
0
1
0
X1
0
0
X2
1
1
1
0
X1
1
0
0
1
X2
X2
0
1
0
1 1
0
1
40
Effect of variable ordering
(a1  b1)  (a2  b2 )  (a3  b3 )
Good Ordering
Bad Ordering
a1
a1
b1
a2
a2
a3
a2
a3
a3
b2
b1 b1 b1 b1
a3
b2 b2
b3
0
a3
b3
1
Linear Growth
0
1
Exponential Growth
41
ROBDD sizes & variable ordering

Bad News 



Good News 




Finding optimal variable ordering NP-Hard
Some functions have exponential BDD size for all
orders e.g. multiplier
Many functions/tasks have reasonable size ROBDDs
Algorithms remain practical up to 500,000 node OBDDs
Heuristic ordering methods generally satisfactory
What works in Practice 


Application-specific heuristics e.g. DFS-based ordering
for combinational circuits
Dynamic ordering based on variable sifting (R. Rudell)
42
Variants of decision diagrams






Multiterminal BDDs (MTBDD) – Pseudo Boolean functions Bn 
N, terminal nodes are integers
Ordered Kronecker FunctionalDecision Diagrams (OKFDD) – uses
XOR in OBDDs
Binary Moment Diagrams (BMD) – good for arithmetic
operations and word-level representation
Zero-suppressed BDD (ZDD) – good for representing sparse
sets
Partitioned OBDDs (POBDD) – highly compact representation
which retains most of the features of ROBDDs
BDD packages –
 CUDD from Univ. of Colorado, Boulder,
 CMU BDD package from Carnegie Mellon Univ.
 In addition, companies like Intel, Fujitsu, Motorola etc.
have their own internal BDD packages
43
Symbolic logic





Symbolic logic deals with the structure of
reasoning
It defines ways to deal with relationships
between concepts
Provides ways to compose proofs of
statements
Provides ways to express statements in a
precise, compact and symbolic manner
More precisely, a formal symbolic logic
consists of



A notation (symbols and syntax)
A set of axioms (facts)
A set of inference rules (deduction scheme)
44
Types of symbolic logic

Propositional Logic – commonly known as
Boolean algebra


First Order Logic


Variables in this algebra  {0,1}
Existential () and Universal () quantifiers over
variables
Higher Order Logic

Existential and Universal quantification over sets
and functions
45
Key features of a theory

Expressiveness


Completeness


All valid formulas are provable
Decidability


What kind of statements can be written in the theory
There exists an algorithm to deduce the truth of any
formula in the theory
Comparison of types of logic

Propositional
 Least expressive, decidable, complete

First Order Logic
 More expressive, decidable, not complete

Higher Order Logic
 Most expressive, not decidable, not complete
46
First-order logic

First-Order Logic


theory in symbolic logic
formalizes quantified statements
 E.g: “there exists an object such that…” or “for all
objects, it is the case that…”

Statements in first-order logic built using:






Variables
x, y
Constants
0, C, 
Functions
f (x ), x + y
Predicates
p (x ), x > y, x = y
Boolean connectives
, , , 
Quantifiers
, 
47
First-order theories

A first-order theory


a set of first-order statements about a related set of
constants, functions, and predicates.
Example:

A theory of arithmetic might include the following
statements about 0 and +:
x. ( x + 0 = x )
x,y. (x + y = y + x )
48
Validity of an expression in a theory

Given


A theory and an expression
Using
Building blocks of that theory
 If expression evaluates to true for every
evaluation, then it is valid in the theory


Example:

X >= 0 is a valid expression in positive
real arithmetic
49
Validity checking & undecidability

Given a theory  in first-order logic and an expression
 we wish to prove that  is valid in 


Validity of  in  is written as  |= 
Undecidability of FOL
 A well-known result states that in general it is undecidable
whether a FOL formula is valid in a given first-order theory



However with appropriate restrictions on  and  the theory
can be made decidable and practical programs can be built
around
Many practical problems can be posed as formulas in
a certain theory or a combination of theories
A proof of validity of this formula results in a solution
to the problem

Example
 Scheduling of complex operations in a manufacturing plant
50
Proof system

A formal proof in a theory



Rewrite rules


Deal with mechanical massaging of statements
irrespective of the meaning of the statements
Key requirement of a proof system


A set of steps of statements
A statement is derived from a previous statement
using a set of defined inference rules
Soundness : All provable formulas are logically
true!
A proof system need not be complete or
decidable in order to be useful!
51
Automated vs. interactive theorem proving
John Rushby, SRI, asserts “There are no fully
automatic theorem provers”.
 For best performance most theorem provers
require user guidance



Variable ordering, weighting of literals, function
symbols, strategy selection, orientation of
equations, invention of ordering lemmas,
induction hints
Automation in certain domains




Propositional logic using SAT solvers, BDDs
Linear arithmetic – integer/linear programming
Temporal logic – model checking
Induction (Boyer-Moore heuristics)
52
Example theorem prover: PVS
• Owre et al., 1992 at SRI
System
model
PVS File
Proofs
Formulae
To be
proved
• System model is translated either automatically or manually
• Formulae to be proved are also translated from their native forms
• Proofs are usually carried out interactively
A
53
PVS Methodology

Automate everything that is decidable


Heuristic automation for obvious cases for
other problems



Propositional calculus, linear arithmetic, finitestate model checking
Hashing conditional rewriter integrated with
decision procedures
Instantiation, induction
Human control for things difficult to
automate


Sequent calculus presentation
Tactic language for defining higher-level proof
strategies
54
Stanford validity checker (SVC)

Started with applications to processor
verification



[Burch and Dill ‘94]
[Jones et al. ‘95]
Applications since release





Symbolic simulation [Su et al. ‘98]
Software specification checking [Park et al. ‘98]
Infinite-state model checking [Das and Dill ‘01]
Theorem prover proof assistance [Heilmann ‘99]
Integration into programming languages
[Day et al. ‘99]
55
Overall flow of SVC

Given an expression whose validity has to be
checked


Choose an atomic formula ƒ in the expression
Case split on the atomic formula
 Create two subformulas, for ƒ = 0, and ƒ = 1
 Simplify the two subformulas
 Iteratively check the validity of the two subformulas

Example: ( x

< y)
(y < x)

(x=y)

Choose f = ( x < y )

Case split on f to get two subformulas
( true )  ( y < x )
Simplify
( false )  ( y < x )  ( x = y )
true
Simplify
(y < x)

(x=y)
56
Example (continued)
(y < x)  (x=y)
 Choose f = ( y < x )
 Case splitting gives two subformulas
true  ( x = y ) Simplify
false  ( x = y )
Simplify
true
(x=y)
 Case splitting on f = ( x = y ) gives two subformulas
true and false
 The only false node is formula:
(x  y)  (y  x)  (x y)
If this formula can be proved unsatisfiable by theory then formula is a tautology
Decision procedure for higher level designs:
Uninterpreted functions with equality

Ignore each functionality in the functions

It is called Logic of Uninterpreted Functions
 Arithmetic operations are handled as symbols

Fucntion returns a value
 If the arguments are the same, it returns the same value
(a=b)(x=y)  [f(a,x)=f(b,y)]
x
y
1
f
c

Y
Y:= if c then x else f(x,y)
0
Very useful for analysis of symbolic simulation results

Equivalence checking: Both send f(b) to x
 Design1: if a=b then x <- f(a) else x <- f(b)
 Design2: x<- f(b)

Transform into formulae
 Design1: ((a=b)->(x’=f(a)))&((~(a=b)->(x’=f(b)))
 Design2: x’=f(b)

Decision procedure similar to SAT confirms Design1=Design2
57
58
How is validity checking done?

The validity checker is built on top of a
core decision procedure for satisfiability
in a theory  of a set of literals in the
theory


A literal is an atomic formula or its negation
The core decision procedure depends on the
theory
 e.g. a Satisfiability Solver can be used for
Propositional Logic

SVC proposes


use of several decision theories targeted to
several theories
gives the strongest decision procedure
59
Need for Multiple Theories

Why are multiple theories needed?

Most real-life problems when cast into a
problem of proving validity of a formula span a
set of theories





Propositional logic
Bit-vectors and arrays
Real, linear arithmetic
Uninterpreted functions & predicates
A decision procedure is

a combination of theories must be able to
combine decision procedures that reason in
each of these theories!
60
Basic formal verification techniques

Equivalence checking: Basics and real tools
(Lecture 3)
 Combinational
 Sequential
 Model (property) checking: Basics (Lecture 4)
 Explicit/implicit state based
 Bounded model checking
Formal Equivalence Checking
Given two designs, prove that for all possible input
stimuli their corresponding outputs are equivalent
Design A
=?
Yes/No
Input
Design B
Product
Machine
61
62
Formal equivalence checking: The targets

Equivalence checking can be applied at or
across various levels
System
Level
Gate
Level
Device
Level
RTL
63
Combinational Equivalence Checking (CEC)






Currently most practical and pervasive
equivalence checking technology
Nearly full automation possible
Designs of up to several million gates
verified in a few hours or minutes
Hierarchical verification deployed
Full chip verification possible
Key methodology: Convert sequential
equivalence checking to a CEC problem!

Match Latches & extract comb. portions for EC
CEC in Today’s ASIC Design Flow
RTL Design
Synthesis &
optimization
CEC
Routing
CEC
DFT insertion
CEC
IO Insertion
CEC
Placement
Clock tree synthesis
64
CEC
CEC
ECO
65
CIRCUIT 1
Solving Seq. EC as Comb. EC
PI
Comb.
Logic
PS1
PO
NS1
PI
MATCH
LATCHES
CIRCUIT 2
Combinational Equiv.
Checking
PS
PS2
PI
Comb.
Logic
NS2
PO
PO
Comb.
Logic 1
NS
Comb.
Logic 2
NS
?
PO =
66
CIRCUIT 1
Combinational EC with BDD and SAT
PI
Comb.
Logic
PS1
PO
NS1
PI
MATCH
LATCHES
CIRCUIT 2
Combinational Equiv.
Checking
PS
PS2
PI
Comb.
Logic
PO
Comb.
Logic 1
NS
Comb.
Logic 2
NS
?
PO =
NS2
PO
Represent logic
functions for this entire
circuit with BDD or SAT
67
Methods for Latch Mapping

Incomplete Methods


Regular expression-based using latch names
Using simulation (Cho & Pixley ‘97):
 Group latches with identical simulation signatures



Group based on structural considerations e.g.
cone of influence
Incomplete run of complete method below
(Anastasakis et al DAC ‘02)
Complete Methods

Functional fixed-point iteration based on Van
Eijk’s algorithm (van Eijk ’95)
Van Eijk’s Method for Latch Mapping
Initial Latch
Mapping
Approximation
PI
Apply Latch
Mapping
Assumptions
Iterate
PS
No
Comb.
Logic 1
NS
Comb.
Logic 2
NS
?
=
Fixed-point ?
Yes
Done !!
Verify Latch
Mapping
Assumptions
68
69
If-Then-Else operation

Concept

Basic technique for building OBDD from logic
network or formula.
Arguments I, T, E
I  T, E
I
X
T
1
MUX
E
0
Functions over variables X
 Represented as OBDDs

Result
OBDD representing
composite function
 (I T)  (I  E)

70
If-Then-Else execution example
Argument I
Argument T
Argument E
Recursive Calls
1
a B1
A1,B1
A1 a
A2,B2
A2 b
c A6
A3 d
A4 0

A3,B2
B2 d
1 A5
A6,B2 A6,B5
c B5
B3 0
1 B4
A5,B2 A3,B4
A4,B3 A5,B4
Optimizations



Dynamic programming
Early termination rules
Apply reduction rules bottom-up as return from recursive calls
 (Recursive calling structure implicitly defines unreduced BDD)
71
Derived algebraic operations

Other operations can be expressed in
terms of If-Then-Else
If-Then-Else(F, G, 0)
And(F, G)
F  G, 0
F
F
X
X
G
1
MUX
G
0
0
If-Then-Else(F, 1, G)
Or(F, G)
F  1, G
F
F
X
X
1
1
MUX
G
G
0
72
Generating OBDD from network
Task:
Represent output functions of gate network as OBDDs.
Evaluation
A  new_var ("a");
B  new_var ("b");
C  new_var ("c");
T1  And (A, 0, B);
If-Then-Else(A, B, 0)
T2  And (B, C);
If-Then-Else(B,C, 0)
Out  Or (T1, T2);
If-Then-Else(A, 1, B)
Network
A
T1
B
Out
C
T2
Out
Resulting Graphs
T1
0
A
B
C
a
b
c
1
0
1
0
a
b
b
1
0
a
T2
b
c
1
0
b
c
1
0
1
73
Solving circuit problems as SAT
a
b
h
f
c
d
g
i
e
Input Vector Assignment ?
Primary Output ‘i’ to 1 ?
74
SAT formulas for simple gates
a
b
c
a
c
b
(c  a )(c  b )(c  a  b)
b
a
(a  b)(a  b )
a
b
c
(c  a)(c  b)(c  a  b )
75
Solving circuit problems as SAT

Set of clauses representing function of each gate

Unit literal clause asserting output to ‘1’
(b  f )(c  f )(b  c  f )
(d  g )( e  g )( d  e  g )
(a  h )( f  h )( a  f  h)
a
b
h
f
c
d
e
g
i
(h  i )( g  i )( h  g  i )
(i )
76
CEC in Practice
Key Observation: The circuits being verified usually
have a number of internal equivalent functions
f
’
x1’x ’
2
f
i1 i2
Check
x1(i1, i2,…in) = x1’(i1, i2,…in)
x2(i1, i2,…in) = x2’(i1, i2,…in)
x k’
x1 x
2
To prove f (i1, i2,…in) = f’ (i1, i2,…in)
xk
xk(i1, i2,…in) = xk’(i1, i2,…in)
in
f(x1, x2,…xk) = f’(x1’, x2’,…xk’)
77
Internal Equiv. Based CEC Algorithm
PI
PS
Comb.
Logic 1
Comb.
Logic 2
PO
NS
Random
Simulation
=?
PO
NS
Gather PENs
Combinational miter
after latch mapping
PENs: Potentially
equivalent nodes, i.e.
nodes with identical
simulation signature
Is there an
unjustified PEN
pair x,y ?
No
Done!
Yes
Refine PEN sets
using counterexample
No
Is
x=y?
Yes
Structurally
merge x,y
78
Anatomy of Typical CEC Tools
Circuit A
Quick
Synthesis
Latch
Mapper
Circuit B
Counter-example
viewer
Error Diagnosis
Engine
Structural methods
Learning
BDD
SAT
ATPG
79
Major Industrial Offerings of CEC




Formality (Synopsys)
Conformal Suite (Verplex, now Cadence)
FormalPro (Mentor Graphics)
Typical capabilities of these tools:





Can handle circuits of up to several million gates flat
in up to a few hours of runtime
Comprehensive debug tool to pinpoint error-sources
Counter-example display & cross-link of RTL and gatelevel netlists for easier debugging
Ability to checkpoint verification process and restart
from same point later
What if capability (unique to FormalPro)
80
Reachability-based Equivalence Checking
Inputs
S0
M1
Outputs
=?
M2
S1


S0
S1


Product Machine
Build product machine of M1 and M2
Traverse state-space of product
machine starting from reset states
S0, S1
Test equivalence of outputs in each
state
Can use any state-space traversal
technique
81
Move to System-Level Design
System-level design
Manual effort
Architecture exploration
Barrier to adoption of
System-level design
Methodology!
RTL
Current design
iterations
Gate-level design
System-Level Verification
Property & Model
Checking
Manual effort
Equivalence
Checking
RTL
Gate-level design
82
83
System-level Synthesis
System-level design
Manual effort
RTL
Gate-level design
Automatic
Synthesis
84
Scope of Today’s EC Technology
Re-encoding of state
scheduling
Sequential
differences
Serial vs parallel interfaces
pipelining
FFs match
Combinational
EC
Data representation differences
Identical data types Composite data types
Bit-accurate
Precision/rounding
differences
85
Upcoming: Transaction-Based EC

The states in RTL that correspond to states
in system-level model (SLM), are referred
to as synchronizing states
Complete
Verification
SLM
Refinement mapping
or
Sequential
counterexample
RTL
Transient states
86
Transactions : State View
SL
transaction
SLM
Refinement mapping
RTL transaction



RTL
Encapsulates one or more units of computation
for the design being verified
Self-contained since it brings the machine back
to a synchronizing state
Some EDA vendor is about to offer a formal
verification tools that can deal with SLM, such
as Calypto
87
Equivalence Checking: Conclusions

Currently equivalence checking based on
latch mapping+CEC




Methodology premised on structural similarity
of designs under comparison
Efficient & scalable
Maybe applicable to system-level problems
More general sequential EC somewhat
less explored
 Might be needed for system level
equivalence checking
88
Model (property) checking: Basics (Lecture 4)

Basic model checking algorthm


States are explicitly represented
States are “implicitly” represented
Symbolic model checking with BDDs
 Model checking using SAT

89
Sequential logic circuit
Y=c(ab)
a
AND
OR
b
y
c
NOT
XOR
Combinational Circuit
Logic Gates
INPUTS
a
o
c
Present
states
b
p
Q D
OUTPUTS
Comb
Logic
LATCHES
n
Sequential Circuit
Next
States
90
Temporal logic model checking
Verify Reactive Systems

Construct state machine representation of reactive system
 Nondeterminism expresses range of possible behaviors
 “Product” of component state machines


Express desired behavior as formula in temporal logic (TL)
Determine whether or not property holds
FSM
rep.
Traffic Light
Controller
Design
True
Property
in some
TL e.g.
CTL, LTL
“It is never
possible to
have a green
light for both
N-S and E-W.”
Model
Checker
False
+ Counterexample
91
MoC: Finite State Machine (FSM)
0/0
INPUTS
Present
states
Comb
Logic
OUTPUTS
Next
States
LATCHES
Mealy FSM: I, S, , S0, O, )






I: input alphabet
S: finite, non-empty set of states
 : S  I  S, next-state function
S0  S : set of initial (reset) states
O: output alphabet
 : S  I  O , output function
S1
1/1
1/1
0/0
S3
S2
1/0
0/0
State Transition Graph
x=0
x=1
S1
S1,0
S2,1
S2
S1,0
S2,0
S3
S3,0
S1,1
State Transition Table
92
Classification of properties

Safety properties



“undesirable things never happen”
“desirable things always happen”
Examples:
 A bus arbiter never grants the requests to two masters
 Elevator does not reach a floor unless it is requested
 Message received is the message sent

Liveness (progress) properties



“desirable state repeatedly reached”
“desirable state eventually reached”
Examples:
 Every bus request is eventually granted
 A car at a traffic light is eventually allowed to pass
93
Fairness constraints



In general, not every run in a state machine is a
valid behavior
But all runs are included in transition systems
Fairness constraints rule out certain runs


Fairness constraints can be expressed as CTL
formulas



Properties only checked for fair paths !!
A fair path must satisfy each formula infinitely often
Path quantifiers are restricted to only the fair paths
Fairness examples


An arbiter arbitrates each requestor infinitely often
In a communication channel a continuously transmitted
message is received infinitely often
94
Temporal logics

Precise specification
 Amenable to symbolic manipulation
 Two kinds of temporal logics (TL)

Linear Temporal Logic (LTL):
 Time is a linear sequence of events

Branching time temporal logic (CTL, CTL*):
 Time is a tree of events

CTL




Formulae describe properties of computation trees
Computation Trees are obtained by unwinding the
transition system model
Branching structure due to nondeterminism
CTL* is more powerful, includes CTL and LTL
95
Syntax of CTL

Every atomic proposition is a CTL formula
 If f and g are formulae then so are










f, (f  g), (f  g), (f  g), (f  g)
AG f - in all paths, in all state f (in all future, f)
EG f - in some path, in all states f
AF f - in all paths, in some state f (in every future f)
EF f - in some future f
A(f U g) - in all paths, f holds until g
E(f U g) - in some path, f holds until g
AX f - in every next state, f holds
EX f - in some next state f holds
Examples




AG ¬ (EW_light_go  NS_light_go)
AG (car_at_intersection  AF(light_green))
AG (EF Restart)
EF (Start  ¬Ready)
96
CTL model checking
(Clarke and Emerson, Quielle and Sifakis)
M╞ F

M: Transition System, F: CTL formulae
 M defines a tree (unwind the transition system)
 F specifies existence of one or all paths satisfying
some conditions
 Verification checks whether these conditions hold
for the tree defined by M
 Specifically:


Compute the set of states of M satisfying F
M ╞ F iff initial states of M are in this set
97
CTL Model checking example 1
P
Compute EFp
EF p = p  EX(p)  EX(EX(p))  . . .
STEP 1
STEP 2
P
P
Fixed Point !!
STEP 3

P


Computation terminates
EF p Holds in all dark states
Computation involves


backward breadth first traversal
Calculation of Strongly
Connected Subgraphs (cycles)
98
CTL Model checking example 2
P
P
P
Compute EG p
EG p = p  EX p  EX(EX p)  . . .
STEP 2
Initial:STEP 1
P
P
P
STEP 3
P
P
P
P
TERMINATION
P
P
P
P
P
99
Checking safety conditions
S0: Initial states



Z : Bad states
Start from S0 (Z) = set of initial (bad) states
Perform forward (backward) reachability analysis
to compute a reached state set R (B)
Determine if R (B) intersects Z (S0)
S
S0
0
B
R
Z
Forward Reachability
Z
Backward Reachability
100
Model checking approaches

Explicit state model checking




Requires explicit enumeration of states
Impractical for circuits with large state spaces
Useful tools exist: Murphi, SPIN, …
Symbolic model checking


Representation & manipulation in terms of ROBDDs
or SAT solvers
Core tasks:
 Represent state machine (transition relation) and sets of
states
 Forward/backward reachability analysis
 Based on computing image/pre-image of set of states
 Fixed-point detection
101
Symbolic manipulation with OBDDs

Strategy

Represent data as set of OBDDs
 Identical variable orderings



Express solution method as sequence of
symbolic operations
Implement each operation by OBDD manipulation
Key Algorithmic Properties



Arguments: OBDDs with identical variable orders
Result is OBDD with same ordering
Each step polynomial complexity
102
If-Then-Else operation

Concept

Basic technique for building OBDD from logic
network or formula.
Arguments I, T, E
I  T, E
I
X
T
1
MUX
E
0
Functions over variables X
 Represented as OBDDs

Result
OBDD representing
composite function
 (I T)  (I  E)

103
If-Then-Else execution example
Argument I
Argument T
Argument E
Recursive Calls
1
a B1
A1,B1
A1 a
A2,B2
A2 b
c A6
A3 d
A4 0

A3,B2
B2 d
1 A5
A6,B2 A6,B5
c B5
B3 0
1 B4
A5,B2 A3,B4
A4,B3 A5,B4
Optimizations



Dynamic programming
Early termination rules
Apply reduction rules bottom-up as return from recursive calls
 (Recursive calling structure implicitly defines unreduced BDD)
104
Derived algebraic operations

Other operations can be expressed in
terms of If-Then-Else
If-Then-Else(F, G, 0)
And(F, G)
F  G, 0
F
F
X
X
G
1
MUX
G
0
0
If-Then-Else(F, 1, G)
Or(F, G)
F  1, G
F
F
X
X
1
1
MUX
G
G
0
105
Generating OBDD from network
Task:
Represent output functions of gate network as OBDDs.
Evaluation
Network
A
A
B
C
T1
T2
Out
T1
B
Out
C
T2






new_var ("a");
new_var ("b");
new_var ("c");
And (A, 0, B);
And (B, C);
Or (T1, T2);
Out
Resulting Graphs
T1
0
A
B
C
a
b
c
1
0
1
0
a
b
b
1
0
a
T2
b
c
1
0
b
c
1
0
1
106
Characteristic functions
Concept

A  {0,1}n
 Set of bit vectors of length n

A
Represent set A as Boolean
function A of n variables
0 /1
 X  A if and only if A(X ) = 1
Set Operations
Union
Intersection
A
A
B
B
107
Symbolic FSM representation
Nondeterministic FSM
Symbolic Representation
n1
00
n2
01
o1
10

o2
o2
0
1
Represent set of transitions as function (Old, New)


11
o1 ,o2 encoded
old state
n1 , n2 encoded
new state
Yields 1 if can have transition from state Old to state New
Represent as Boolean function

Over variables encoding states
108
Reachability analysis
Task



Compute set of states reachable from initial state Q0
Represent as Boolean function R(S)
Never enumerate states explicitly
Given
old state
Compute

state
0/1
new state
Initial
R0
=
Q0
R
0/1
109
Breadth-First reachability analysis
00
01
R
R00
00
00
00
10
R
R11
01
01
R
R22 R3
10
10
11
Ri – set of states that can be reached in i
transitions
 Reach fixed point when Rn = Rn+1


Guaranteed since finite state
110
Iterative computation
Ri

old
new
Ri +1

Ri
R 0  Q0
do
Ri  1(s)  Ri(s)  s ' [ Ri(s' )   (s' , s)]
i  i 1
until Ri  Ri  1
ALGORITHM
111
BDD-based MC: Current status

Symbolic model checkers can analyze
sequential circuits with ~200- 400 flip flops


Challenges



For specific circuit types, larger state spaces have
been analyzed
Memory/runtime bottlenecks
Adoption of TLs for property specification
Frontier constantly being pushed




Abstraction & approximation techniques
Symmetry reduction
Compositional reasoning
Advances in BDD technology …
112
Solving circuit problems as SAT
a
b
h
f
c
d
g
i
e
Input Vector Assignment ?
Primary Output ‘i’ to 1 ?
113
SAT formulas for simple gates
a
b
c
a
c
b
(c  a )(c  b )(c  a  b)
b
a
(a  b)(a  b )
a
b
c
(c  a)(c  b)(c  a  b )
114
Solving circuit problems as SAT

Set of clauses representing function of each gate

Unit literal clause asserting output to ‘1’
(b  f )(c  f )(b  c  f )
(d  g )( e  g )( d  e  g )
(a  h )( f  h )( a  f  h)
a
b
h
f
c
d
e
g
i
(h  i )( g  i )( h  g  i )
(i )
115
SAT-based unbounded MC

SAT-based Inductive reasoning
 Exact image computation


Use SAT solver just for fixed-point detection
Image computation using SAT solver
 McMillan CAV’02, Kang & Park DAC’02

Approximate image computation


Using Craig Interpolants (McMillan CAV’03)
Abstraction refinement
 Discussed later in the tutorial
116
SAT-based reasoning on ILAs
PI
PO
CL
BMC work (Biere et al)
NS
PS
Unroll
k-Steps
 Popularized by the

Current SAT solvers
have shown good results
LATCHES
PI1
PI2
PI
k
PS1
CL1
PO1
NS1
PS2
CL2
PO2
NS2
NSk-1
PS3
PSk
CLk
POk
NSk
117
SAT-based inductive reasoning
 I0
never satisfies ~ P
Simple Induction
UNSAT


‘1
’
I0
Induction
Step
Base Case
P
P
+
AG P is TRUE
UNSAT
‘1’
‘1’
CLk+1
P
‘1
’
If Ii never satisfies ~ P, then Ii+1 never satisfies ~P
It is never the case that (I0 satisfies P) and (Ii+1
satisfies ~P)
118
SAT-based inductive reasoning
P
I0
Induction
Step
Base Case
P
CL1
P
P
CL2
CLk
‘1
’
P
‘1’
P
CL1
‘1’
P
‘1’
CLk
CLk+1
Induction with depth ‘k’
(Sheeran et al, Bjesse et al FMCAD 2000)
P
‘1
’
119
SAT-based induction

Can prove or disprove properties
 k-depth induction:



Can check more properties for larger k
Base case is simply k-length BMC
But not complete !
Example:
P
Not k - depth
inductive for
any k !
P
Unreachable
state-space
120
SAT-based inductive reasoning

Unique paths Induction:







Restrict unrolled ILA to be loop-free
Sheeran et al, Bjesse et al FMCAD’00
Unrolling upto recurrence diameter
i.e. length of longest loop-free path
Complete!
Stronger induction methods can be expensive
But, some properties very easy to prove by
induction, very hard by state-space traversal
Simple induction can be cheap, first step in
verification flow
121
SAT-based image computation
i0
R0( s)  Init
Issues:
 Function representation
 Quantification
do
Ri  1(s' )  toProp(s.Tr (s, s' )  Ri (s))
i  i 1
until Ri(s)  P(s) or
i 1
i
 R ( s)   R ( s)
k
k 0
k
k 0
SAT
Solver
Bug found !
Fixed-point
122
Function Representation


Representation of: Init, Ri(s), P(s), Tr(s,s’)
Converted to CNF for SAT solving
b





x



z
y
Reduced Boolean Circuit (RBC)
Abdulla et al, TACAS 2000
b
a
0
1
Boolean Expression Diagram (BED)
Williams et al, CAV 2000
123
Quantification

Apply definition of existential quantification:
x. ( x)   ( x  0)   ( x  1)
 Mitigate formula blow-up by:


Inherent reduction rules of function rep.
Special case quantification rules:
Inlining:
x.(x   )   ( x)   ( )
where x  Vars( )
Scope Reduction:
x. ( x)   (x. ( x)) 
where x  Vars( )
x. ( x)  ( x)  (x. ( x))  (x. ( x))

Limitation: Suitable only when small number
of variables to be quantified
124
Exact image computation using SAT
McMillan, CAV 2002
CTL Model Checking
procedure AG(p)
Let Z = Q = p
while Z  1
let Z = (W · pi/si)Q
let Q = Q  Z
return Q
Solve W · f
Solution:


Express f in CNF: fCNF
Drop all wi literals from
fCNF
Core problem: Express a given formula f in CNF
125
Computing a CNF representation for f
Basic Algorithm
 Create CNF(f)
 Solve SAT(CNF(f)  vf)
 Compute blocking
clause for each
satisfying assignment
 Collect all blocking
clauses  fCNF
Blocking Clauses Must:

Contain only original vars. of f
 Be false under some sat. assgn.
of CNF(f)  vf
 Be implied by CNF(f)  vf
e.g. f = (ab)c
a
b
vab
vf
c
CNF(f)
Blocking
Clauses : (bc) , (ac)
fCNF= (bc) (ac)
126
Some issues

Issues:

Blocking clauses expressed in terms of original
variables of f
 Extracted from a separate implication graph


Quantification of W vars. can be performed on
each generated blocking clause: Combine both
steps into one!!
Conclusions:



Technique promising where BDDs blow up
BDDs superior as a general purpose technique
Proposed technique needs more polishing
127
Lecture 5

Enhancing formal verification capacity
Abstraction-refinement
 Assume guarantee/Compositional
Reasoning
 Approximation
 Symmetry reduction
 Partial Order Reduction


Industrial and research tool offerings
128
Abstraction

Limitations of symbolic model checking

Suffers from state explosion
 Concurrency
 Data domains

Abstraction of state space

Represent the state space using a smaller model
Pay attention to preserving the checked properties.

Do not affect the flow of control.

129
Example

Use smaller data objects
 HDL Code:
X:= f(m);
Y:=g(n);
if (X*Y>0)
then …
else …
X, Y never
used again.



Assign values {-1, 0, 1} to X and Y.
Based on the following connection:
sgn(X) = 1 if X>0,
0 if X=0, and
-1 if X<0.
sgn(X)*sgn(Y)=sgn(X*Y).
Change f and g to produce abstract
values for X and Y
130
Abstraction vs. simplification
Not every simplified system is an
abstraction
 The key question is:


If we prove or disprove a property of the
simplified system, what have we learned
about the original system?
131
Abstraction (Cont)

Abstract transition relation is conservative


Abstract next states must contain all concrete
successors
And possibly more states
t
RA
s
Abstract
g
g
Concrete
x
y
RC
132
Abstract counter-example

If model checking fails an abstract counterexample is produced
 Concrete transitions are present for each
pair of consecutive abstract states

But concrete counter-example may not be
present!
Spurious Trace
Abstract
Concrete
g
g
g
y’
Real Trace
x
y’’
z
133
Abstraction refined

Abstraction is refined by adding more states


prevents previous spurious counter example
Model checking is repeated on new
abstraction

iterate
New Trace
gi
Abstract
Concrete
gi
gi
gi
y1
Real Trace
z
x
y’’
134
Abstraction refinement algorithm
Build
abstract model
Refinement
spurious
counterexample
Model
check
abstract
model
true
True on
concrete model
abstract
counterexample
abort
Infeasible
Check
abstract
counterexample
on concrete
model
real
counterexample
False on
concrete model
135
Assume-Guarantee Reasoning

S and R are just too large to be verified at the
same time
 Like to verify S and R separately !
Sender
S
||
Receiver
has
R
<
Property
136
Assume-Guarantee Reasoning

First try to find something intermediate, S’ and
R’ between the designs and the specification,
such that it is easy to verify that S’ and R’
satisfy the property
S
R
<
S’
R’
<
137
Assume-Guarantee Reasoning

If we can verify individual cases separately, we
are done !
R
S
S
R
<
R’
<
S’
<
S’
R’
<
138
Assume-Guarantee Reasoning

But normally we cannot due to unconstrained
inputs
Inputs are
unconstrained
S
S
<
R’
Inputs are
<
unconstrained
S’
R
R
<
S
R
<
139
Assume-Guarantee Reasoning

Use S’ and R’ to constrain inputs !
S’
R
<
R’
S
R’
<
S’
S
R
<
S’
R’
<
140
Assume-Guarantee Reasoning

This is a theorem !AG reasoning: Example
S &
R
->
R
S
&
R
->
S
S
&
R
->
S & R
141
Symmetry reductions
Idea: If state space is symmetric, explore only
a symmetric “quotient” of the state space
A permutation function f : S  S
is an automorphism if:
( x, z)  ( f(x), f(z))
0,0
0,1
1,0
e.g. f: f(0,0) = 1,1 f(1,1) = 0,0
f(0,1) = 0,1 f(1,0) = 1,0


The set of all automorphisms forms
a group!
Automorphism groups induce
equivalence classes (orbits) over
the state space
1,1
e.g. [ (0,0), (1,1) ]
[ (0,1), (1,0) ]
142
Quotient machine
0,0
0,1
[ (0,0),(1,1) ]
1,0
[ (0,1), (1,0) ]
1,1

Map each state to its representative in
the orbit
Quotient machine
 Do model checking analysis on the
quotient machine
143
Symmetry reductions

Difficulty



Solutions



Identifying symmetry groups
Computing function mapping states to
representatives
Ask user to tell you where the symmetries are
Be satisfied with multiple representatives for
each orbit
Tools: Mur, Nitpick, RuleBase
144
Over-approximate reachability

Exact reachability captures the exact reachable
state-space


Problem: BDD-blowup in many real designs
Solution: Compute over-approximation of the
reachable states
R+
R2
I0
Error could be a false
negative

+
R1+
R1
R2
Often sufficient to prove
properties correct

R
Can trade off BDD-size
and runtime with accuracy
of approximation

145
Over-approx. reachability techniques

Split FSM into submachines by
partitioning statevars
 Perform (exact)
reachability on each
machine
 Cross-product of
reached state
spaces gives overapprox. for original
FSM
PI
PS
CL
LATCHES
X
PO
NS
X
146
Over-approx: more issues

Communicate between sub-FSMs to
tighten approximation



After each time-frame
After least fixpoint computation for a sub-FSM
Computing partitions



Heuristic and/or manual
Disjoint partitions (Cho et al)
Overlapping partitions (Govindaraju et al)
 Can capture limited interaction among sub FSMs
 Tighter approximation
 May not increase BDD sizes much
147
Partial order reduction

Factor out independent state transitions!
(typical for asynchronous communication
as in Software- and Protocol-Checking)
 May result in exponential reduction
in the number of states
Process
A
transition
Process
B
transition
One Relevant Trace of States
Synchronization
148
Model Checkers - Research Tools
SMV (CMU, Cadence)
 VIS (UC Berkeley)
 Mocha (UC Berkeley, compositional
reasoning)
 Verisoft (AT&T, C-model checker)
 Bandera (Java model checker)

149
Industrial Model Checkers

FormalCheck (Cadence)




COSPAN (from Bell Labs) under the hood
Support for arbitrary precision arithmetic
Automatic bus-contention, multi-driver violation, tristate support fir high-impedance check
Powerful design reduction techniques
 Removal of portions of design that do not affect the
property being proven
 Constant & constraint propagation
 Iterative reduction guarantees that queries proven on the
reduced design hold on the entire design
150
EDA Vendor Tool Offerings

Verplex (Cadence) Blacktie
 IBM RuleBase
 @HDL - @Verifier





Real Intent Verix


works on Verilog RTL
static assertion checks
automatic property extraction
clock domain synchronization errors
slimilar to @Verifier
Averant Solidify
 Jasper design automation Jasper Gold
151
Lecture 6: Semi-formal verification
C
o
v
e
r
a
g
e
Existing
Formal
FV Augmented
Simulation
(Falsification)
Verification
Manual test
w/ coverage
2K
20K
FV
+ Complete coverage
- Limited capacity
200K
2M
FV Augmented Simulation
+ Good coverage
+ Good capacity
Random
simulation
GATES
Simulation
+Unlimited capacity
- Poor coverage
152
Section outline
Symbolic simulation
 Symbolic trajectory evaluation (STE)
 SAT-based bounded model checking
 Sequential ATPG-based model
checking
 Guided search
 Smart simulation

153
Symbolic simulation

Conventional simulation:

Input & outputs are constants (0,1,X,…)
1 a
0 b
1

c
1
a·b+b·c
Problem: Too
many constant
input combinations
to simulate !!
Symbolic simulation:



Symbolic expressions used for inputs
Expressions propagated to compute outputs
Equivalent to multiple constant simulations !!
Ref: Prof. David Dill, CAV ’99c
154
Symbolic simulation (sequential case)
a0
a0·b0 + b0 ·c
a1
a1·b1+
b1·(a0·b0 + b0·c)
b1
b0
Time
frame 1
c
Time
frame 2
a0·b0 + b0·c
a1
a0
b1
b0
c
a1·b1+
b1·(a0·b0 + b0·c)
Unrolled Circuit
155
Symbolic simulation
Inputs can be
constants
1
b+c
b
a
a·b + b ·c
b
c
c



a+b
Simulate certain set
Input
expressions
of patterns
b
can
be
related
Model signal
correlations
Can result in simpler
output expressions
b+c
c
156
Symbolic simulation

Use BDDs as the symbolic representation
 Work at gate and MOS transistor level
 Can exploit abstraction capabilities of ’X’
value




Can be used to model unknown/don’t care
values
Common use in representing uninitialized state
variables
Boolean functions extended to work with {0,1,X}
Two BDD (binary) variables used to represent
each symbolic variable
157
Symbolic simulation
Advantages




Can handle larger designs than model checking
Can use a large variety of circuit models
Possibly more natural for non-formalists.
Amenable to partial verification.
Disadvantages


Not good with state machines (possibly better
with data paths).
Does not support temporal logic
 Requires ingenuity to prove properties.
158
Practical deployment

Systems:




COSMOS [bryant et al], Voss[Seger et al Intel]
Magellan [Synopsys]
Innologic
Exploiting hierarchy

Symbolically encode circuit structure
 Based on hierarchy in circuit description

Simulator operates directly on encoded circuit
 Use symbolic variables to encode both data values &
circuit structure


Implemented by Innologic, Synopsys (DAC ‘02)
Greatest success in memory verification
(Innologic)
159
High-level symbolic simulation

Data Types: Boolean, bitvectors, int, reals, arrays

Operations: logical, arithmetic, equality,
uninterpreted functions

Final expression contains variables and
operators
Coupled with Decision procedures to check
correctness of final expression
Final expressions can also be manually checked
for unexpected terms/variables, flagging errors
e.g. in JEM1 verification [Greve ‘98]


160
High-level symbolic simulation

Manipulation of symbolic expressions done
with



Rewrite systems like in PVS
Boolean and algebraic simplifiers along with
theories of linear inequalities, equalities and
uninterpreted functions
Extensively used along with decision
procedures in microprocessor verification




Pipelined processors: DLX
Superscalar processors: Torch (Stanford)
Retirement logic of Pentium Pro
Processors with out of order executions
161
Symbolic trajectory evaluation (STE)

Trajectory : Sequence of values of system
variables


Example: c = AND (a, b) and delay is 1
A possible trajectory : (a,b,c) = (0, 1, X), (1, 1, 0),
(1, 0, 1), (X, X, 0), (X, X, X),…

Express behavior of system model as a set
of trajectories I and desired property as a
set of trajectories S
 Determine if I is inconsistent with S


Inconsistent: I says 0 but S says 1 for a signal
at time t
Consistent: I says 0 but S says X or 0 for a
signal at time t
162
STE: An example
4-Bit Shift Register
Din
Specification
Dout
Assert
Din = a  NNNN Dout = a
If apply input a
then 4 cycles later
will get output a
Din
Din
Din
Din
Din
Ref: Prof. Randal Bryant, 2002
a
X
X
X
X
X
X
a
X
X
X
X
X
X
a
X
X
X
X
X
X
a
X
X
X
X
X
X
a
a
Din = a

T=0
Dout
T=1
Dout
T=2
Dout
T=3
Dout
T=4
Dout
NNNN Dout = a
Check
163
STE: Pros, cons & u

Advantage: Higher capacity than symbolic
model checking
 Disadvantage: Properties checkable not as
expressive as CTL
 Practical success of STE




Verification of arrays (memories, TLBs etc.) in
Power PC architecture
x86 Instruction length decoder for Intel processor
Intel FP adder
Microprocessor verification
164
SAT-based bounded model checking
Property F
FSM M
PI
PO
CL
NS
PS
Example F: AG P
P
?
LATCHES
Question: Does M have a counter-example to F
within k transitions ?
Biere et al (TACAS’99, DAC’99)
165
SAT-based bounded model checking
P
P
P
I0
CL1
CL2
CLk
P
‘1
’
Unroll M for k time-frames
SAT
CNF
SAT
Solver
UNSAT
Counter-example
to AG P
No Counterexample within k
steps
166
SAT-based BMC

Primarily used for finding bugs !
 Verification complete if k > sequential
depth of M
Open


Sequential depth computation or tight problem!!
estimation intractable in practice
Can express both safety and liveness
properties (bounded semantics)


All LTL formulas
Unbounded fairness by detecting loops
167
SAT-based BMC: Pros & cons

Advantages:




SAT-BMC good at producing counter-examples upto
medium depths (upto 50-60)
SAT solvers less sensitive to size of design: SATBMC can handle larger designs
SAT solvers require less parameter tuning:
Productivity gain
Drawbacks:



Incomplete method: Cannot verify properties
Ineffective at larger depths: Slow, CNF blow-up
Cannot describe all CTL properties
168
Enhancements to basic SAT-BMC

CNF generation for BMC




Decision variable ordering



Bounded cone-of-influence: Biere et al CAV’99
Circuit-graph compression: Ganai et al VLSID’02
Binary time-frame expansion: Fallah ICCAD’02
BMC-specific static ordering: Strichman CAV’00
Tuning VSIDS for BMC: Shacham et al MTV’02
Addition of clauses/constraints



Sharing clauses across BMC runs: Strichman CHARME’01
Learning clauses from BDDs: Gupta et al DAC’03
Using BDD reachability over-approx: Cabodi et al DATE’03
169
Sequential ATPG for MC

Proposed by Boppana, Rajan, Takayama & Fujita, CAV ‘99
e.g. AG p
INPUT
EF p
INPUT
AUTOMATA
CIRCUIT
from property
CIRCUIT
TEST
NETWORK
p
stuck-at fault
s-a-0 fault
170
Advantages of sequential ATPG-based MC
vs SAT-BMC
vs BDDs



No explicit storage of
states
No need to build
transition relation
Good balance of DFS
and BFS traversal of
state-space



Can model real-world
primitives, e.g. tri-state
buses, high impedence
value
No explicit unrolling of
time-frames
Uses circuit-based
heuristics to guide or
speed-up search
171
Sequential ATPG for BMC
PROPERTY


n
Recent work
stuck-at
by Abraham
fault
TEST
ORIGINAL
MONITOR
NETWORK
CIRCUIT
et al (ITC’02,
VLSID’03)
Model both
p
safety &
p
p
p
start
p
p
liveness
…
n
2
0
1
n-1
properties
Example:
p
(bounded)
p
EG p
p
172
ATPG-MC: Current status




Attempts to use simulation-based ATPG for
falsification (Hsiao et al HLDVT’01, DAC’02)
No research characterizing fragment of language
(e.g. CTL, LTL) checkable through ATPG-based MC
Some works report dramatic improvements of seq.
ATPG-BMC vs. SAT-BMC
Current efforts towards combining SAT solvers
and sequential ATPG (SATORI ICCAD’03)
173
Guided search

State-space search optimized for bugsearching (Yang & Dill, DAC 98)
 Use prioritized search

Cost function to pick next state to search
 Hamming distance to error states
Breadth-first Search
Prioritized Search
Error State
Error State
174
Improving guided search

Target enlargement
also Yuan et al CAV 97

Without
Target
Enlargement
Reset
State
Improved cost function

Tracks
 Compute series of approximate
preimages
 Use the approximate pre-image to
estimate distance to enlarged target

Guideposts
 Designer provided hints/necessary
pre-conditions for assertion violation
 Bias search to explore search with
those pre-conditions
Error
States
Enlarged
Error
States
175
Smart simulation I : SIVA
[Ganai, Aziz, Kuehlmann DAC ‘99]


Combines random simulation with BDDs and
combinational ATPG
Identify targets


Indicator variables, coverage goals, fail states etc.
Lighthouses:
 Several per target
 “Sub-targets” to guide SIVA to reach a target


At each state identify targets with constant
simulation signature
Advance simulation by visiting states which
causes such targets to toggle value

Search for such next state by ATPG/BDDs
176
SIVA - a run
R1’
R1
R5000’
INITIAL
R2
RANDOM
R5000
BDD
D1’
ATPG
D1
D2
Key: Determination of appropriate targets,
lighthouses etc. to guide the search
177
Smart simulation II: Magellan
[Ho et al, ICCAD 2000 (Synopsys)]

Coverage-driven test generation



Test generation


Identify few interesting signals (typically <64):
coverage signals
Goal: Maximize state-coverage on coverage
signals
Interleave random simulation with symbolic
simulation & SAT-BMC
Unreachability analysis (under-approx)

Identify unreachable coverage states to reduce
coverage target
178
Magellan methodology
Initial
state
Symbolic
simulation /
SAT-BMC

Random
simulation
Coverage
state
Random simulation: Deep narrow search
 SAT-BMC: Short-range exhaustive (wide) search (<10 steps)
 Symbolic simulation: Middle range exhaustive (wide) search
(10-50 steps)
179
Smart simulation III: 0-in search

Approach: Test amplification
 Identify “seed states” reached through
simulation i.e. directed or random simulation
 Explore exhaustively behavior around seed
states using formal methods

SAT-BMC, BDDs, symbolic simulation
+
Formal
=
Simulation
0-In Search
180
Methodology: Assertion-based Verification

Use checkers (written in HDL) to:

Specify targets for simulation/formal methods
 Capturing buggy conditions

Specify environment of a module
 Can be synthesized into constraints


Specify interfaces between components
Inserting checkers:



From 0-in CheckerWare library (~60 checkers)
Specified by the user in Verilog
Created automatically from RTL directives
 By 0-in Check functional tool

Suggested by 0-in Checklist while analyzing RTL
 A kind of sophisticated lint checking
181
0-in search: Tool flow
Instrumented
Verilog RTL
Verilog Tests
and Testbench
Verilog Files with
0-in Checkers
Standard Verilog
Simulator
Source: 0-in Design
Automation Verification
White-paper
No firings in
Verilog output
Simulation
Trace (Seed)
Checker
Control File
0-in Search
0-in Confirm
Verilog simulator
(Firing Replay)
Firings Log
0-in View GUI
Standard
Waveform Tool
Lecture 7: Formal verification in C-based
(SpecC/SystemC) based design methodology
182

C based design
descriptions from
specification (functional)
level down to RTL
 Incremental refinement on
the C/C++ descriptions
 Equivalence checking
between refinements



Between sequential and
parallel descriptions
Between two same control
structures
Equivalence checking between two descriptions
Model checking on each description
Specification
in C
Refined description
for hardware parts
Software parts
remain the same
Removal of pointer,
recursive calling
Refined description
with concurrency
Introduction of
concurrency
(SpecC or SystemC
may be used here)
To RTL
design
: Refinement step
Figure 1. C-based system design flow
Property checking on each
refinement
Please note that in system level designs, both SpecC and SystemC
have similar description mechanisms
183
Execution semantics in SpecC

Sequentiality rule:
Tstart(B1) <= Tstart(a) < Tend(a) <=
Tstart(b) < Tend(b) <=
Tstart(c) < Tend(c) <= Tend(B1)
 Sequential execution within a thread

Example
behavior B1
{ void main(void)
{ a.main();
b.main();
c.main();
}
};
B1
a
b
c
time
184
Execution semantics in SpecC (cont.)

Sequentiality rule:
Tstart(B) <= Tstart(a) < Tend(a) <=
Tstart(b) < Tend(b) <=
Tstart(c) < Tend(c) <= Tend(B)
Tstart(B) <= Tstart(d) < Tend(d) <=
Tstart(e) < Tend(e) <=
Tstart(f) < Tend(f) <= Tend(B)

Example: concurrency/pallalelism
behavior B
{ void main(void)
{ par { b1.main();
b2.main();}
}};
behavior B1
{ void main(void)
{ a.main();
b.main();
c.main();} };
behavior B2
{ void main(void)
{ d.main();
e.main();
f.main();} };
Possible Schedule
B
d
e
a
f
b
c
time
185
Synchronization semantics

wait/notify rule in time-interval formalism:


wait cannot proceed until it receives a notified
event
notified event is valid
until a wait or waitfor statement is reached
behavior A: a.main(); wait e1; b.main();
behavior B: c.main(); notify e1; d.main();

Example:

Notify-wait rule derives: Tend(w) >= Tend(n)
 wait cannot proceed until it receives notified event
‘wait e1’ starts
thread
A
a
‘wait e1’ succeeds
w
b
this order is guaranteed!
B
c
n
‘notify e1’ done
d
time
186
Incremental refinement steps

Starting with a functional model, make each part more
detailed

A1, B1, and C1 are refinement of A, B, and C respectively
void A() {
A
}
void B() {
void A1() {
}
void B1() {
B
}
void C() {
}
void main() {
A();
B();
C();
}
A1
B1
}
void C1() {
C
}
void main() {
A1();
B1();
C1();
}
C1
187
Incremental refinement steps

Change of control structures


IF-THEN-ELSE
Sequential to parallel
void A1() {
A1
void A1() {
A1
}
void B1() {
}
void B1() {
B1
}
void C1() {
}
void main() {
A1();
B1();
C1();
}
}
void C1() {
C1
}
void main() {
par{
A1.main();
B1.main();
}
C1.main();
}
B1
notify
wait
C1
188
Incremental refinement steps

Again make each part more detailed
 A2, B2, and C2 are refinement of A1, B1, and C1
respectively
void A1() {
void A1() {
A1
}
void B1() {
}
void C1() {
}
void main() {
par{
A1.main();
B1.main();
}
C1.main();
}
B1
notify
wait
C1
A2
B2
}
void B1() {
notify
}
void C1() {
}
void main() {
par{
A1.main();
B1.main();
}
C1.main();
}
wait
C2
Equivalence checking of two
descriptions with same control

189
If A and A1, B and B1, C and C1 are equivalent, then
entire descriptions are equivalent

Comparison of two “similar” descriptions
void A() {
void A1() {
A
}
void B() {
}
void C() {
}
void main() {
par{
A.main();
B.main();
}
C.main();
}
B
notify
wait
C
A1
}
void B1() {
}
void C1() {
}
void main() {
par{
A1.main();
B1.main();
}
C1.main();
}
B1
notify
wait
C1
Equivalence checking between
sequential and parallel versions

190
Based on synchronization verification, prove
equivalence

Extraction of synchronization and dependency analysis
void A() {
A
void A() {
A
}
void B() {
}
void B() {
B
notify
wait
B
}
void C() {
}
void main() {
A();
B();
C();
}
}
void C() {
C
}
void main() {
par{
A.main();
B.main();
}
C.main();
}
C
notify-wait pair
are supposed to
communicate !
Symbolic simulation in higher-level
designs

Symbolic execution of designs
All variables and operations are expressed
as symbols
 Expressions among them are also symbols


Efficient simulation for all possible input
patterns

A symbol expression (a + b) requires many
patterns in conventional Boolean level
symbolic simulation
 256 * 256 patterns when a, b are 8-bit variables
191
192
Symbolic simulation example

Example of equivalence checking based on
symbolic simulation


Checking (add1 == add2) , when v1, v2 are
equivalent in both designs
Equivalent variables are collected into EqvClass
a = v1;
b = v2;
add1 = a + b;
Description 1
add2 = v1 + v2;
Description 2
Symbolic simulation
EqvClass
We are going to check the equivalence
between add1 and add2
193
Symbolic simulation example

Example of equivalence checking based on
symbolic simulation


Checking (add1 == add2) , when v1, v2 are
equivalent in both designs
Equivalent variables are collected into EqvClass
a = v1;
b = v2;
add1 = a + b;
Description 1
Symbolic simulation
E1 (a, v1)
E2 (b, v2)
E3 (add1, a+b)
add2 = v1 + v2;
EqvClass
Description 2
Description1 is simulated
194
Symbolic simulation example

Example of equivalence checking based on
symbolic simulation


Checking (add1 == add2) , when v1, v2 are
equivalent in both designs
Equivalent variables are collected into EqvClass
a = v1;
b = v2;
add1 = a + b;
Description 1
Symbolic simulation
E1
E2
E3
E4
(a, v1)
(b, v2)
(add1, a+b)
(add2, v1+v2)
add2 = v1 + v2;
EqvClass
Description 2
Description2 is simulated
195
Symbolic simulation example

Example of equivalence checking based on
symbolic simulation


Checking (add1 == add2) , when v1, v2 are
equivalent in both designs
Equivalent variables are collected into EqvClass
a = v1;
b = v2;
add1 = a + b;
Description 1
add2 = v1 + v2;
Description 2
Symbolic simulation
E1
E2
E3
E4
(a, v1)
(b, v2)
(add1, a+b)
(add2, v1+v2)
EqvClass
Due to the equivalences
in E1, E2
196
Symbolic simulation example

Example of equivalence checking based on
symbolic simulation


Checking (add1 == add2) , when v1, v2 are
equivalent in both designs
Equivalent variables are collected into EqvClass
a = v1;
b = v2;
add1 = a + b;
Description 1
add2 = v1 + v2;
Description 2
Symbolic simulation
E1 (a, v1)
E2 (b, v2)
E3’ (add1, a+b,
add2, v1+v2)
EqvClass
E3 & E4 are merged
into E3’
197
Program slicing for SpecC/C++

Program slicing



Two types of slicing



Can extract a portion of a program based on
dependence analysis
Can be applied to formal methods, since it can
reduce problems to be analyzed
Backward slicing … extracting the portion that can
affect a variable at a certain line of codes
Forward slicing … extracting the portion that can be
affected by a variable at a certain line of codes
Based on C/C++ slicer, SpecC/SystemC/VHDL
slicer can be developed [Shankar et al.]

Since they are similar to C/C++, a little bit of
extension is sufficient
198
Backward slicing

Backward slicing for a variable v extracts all
codes that affect the variable v
Backward slicing
a = 2;
a = 2;
b = 3;
b = 3;
c = 5;
c = 5;
a = a + 10;
a = a + 10;
b = a * c; /start/
b = a * c; /start/
c = c + a;
c = c + a;
a = a * b;
a = a * b;
199
Forward slicing

Forward slicing for a variable v extracts all
codes that are affected by the variable v
Forward slicing
a = 2;
a = 2;
b = 3;
b = 3;
c = 5;
c = 5;
a = a + 10;
a = a + 10;
b = a * c; /start/
b = a * c; /start/
c = c + a;
c = c + a;
a = a * b;
a = a * b;
Example : Interprocedural slicing
with summary edge
200
main()
int sq(int x){
return(x*x);
}
void main(void){
int a,b,c,d;
a=1;
b=sq(a);
c=3;
d=sq(c);
write(d);
}
a=1
call sq()
c=1
b=sq$result
call sq()
A_In x
d=sq$result
A_Out
sq$result
A_In x
write(d)
A_Out
sq$result
sq()
F_In x
x*x
F_Out
sq$result
Control
Dependence
Data
Dependence
Summary
Edge
Call Edge
param in/out
Source code
Dependence graph
Example : Interprocedural slicing
with summary edge
201
main()
int sq(int x){
return(x*x);
}
void main(void){
int a,b,c,d;
a=1;
b=sq(a);
c=3;
d=sq(c);
write(d);
}
1st stage
a=1
call sq()
c=1
b=sq$result
call sq()
A_In x
d=sq$result
A_Out
sq$result
A_In x
write(d)
A_Out
sq$result
sq()
F_In x
x*x
F_Out
sq$result
Control
Dependence
Data
Dependence
Summary
Edge
Call Edge
param in/out
Source code
Dependence graph
Example : Interprocedural slicing
with summary edge
202
main()
int sq(int x){
return(x*x);
}
void main(void){
int a,b,c,d;
a=1;
b=sq(a);
c=3;
d=sq(c);
write(d);
}
2nd stage
a=1
call sq()
c=1
b=sq$result
call sq()
A_In x
d=sq$result
A_Out
sq$result
A_In x
write(d)
A_Out
sq$result
sq()
F_In x
x*x
F_Out
sq$result
Control
Dependence
Data
Dependence
Summary
Edge
Call Edge
param in/out
Source code

Dependence graph
Dependence graph gives all dependency
informations on the programs and is used here
Equivalence checking of C descriptions
based on symbolic simulation

203
Problem

Symbolic simulation of a whole design takes
a very long time, when the design is large
 Computational efforts exponentially increase with
the numbers of conditional branches

Solution

Reducing areas to be simulated symbolically
 Based on difference between descriptions
 See the following slide for intuitive explanation

Textual differences may become a good hint
to identify which portions of programs are
different
204
Efficient equivalence checking in SpecC/C++

Comparison of two similar design descriptions



Extract textual differences
Dependence analysis by program slicing type
techniques
Symbolically simulate the real difference and analyze
the results
: textual
differences
return a;
Description1
return a;
Description2
return a;
Description1
return a;
Description2
205
Verification flow
Desc. 1
Desc. 2
Definition of Input/Output Variables
and Program Slicing
Identification of the Textual Differences
& Extracting Functions to be Checked
Symbolic Simulation
Report of Results
A Naïve way is to simulate both
descriptions separately. Following
slide introduces a more efficient
simulation method
206
More efficient simulation method

A lot of internal equivalence checking are
carried out during verification


Most of them do not directly contribute to
prove output equivalence
More efficient simulation method

Do not simulate the descriptions separately
 Both descriptions are simulated in parallel

Utilizing textual correspondence
 Only checking equivalence of corresponding
statements

Utilizing textual difference
 Equivalence checking can be skipped if two
statements are obviously equivalent
207
An example of verification
a_1 = 3 * in2_1;
b_1 = 360 + in1_1;
c_1 = 2408 * (in1_1 + in2_1);
d_1 = c_1 – 4017 * b_1;
e_1 = 1108 * (a_1 + b_1);
out_1 = (d_1 + e_1) >> 8;

D
E
E
E
E
E
a_2 = in1_2 * in2_2;
b_2 = 360 + in1_2;
c_2 = 2408 * (in1_2 + in2_2);
d_2 = c_2 – 4017 * b_2;
e_2 = 1108 * (a_2 + b_2);
out_2 = (d_2 + e_2) >> 8;
1st line: textually different



Note:
Input: in1, in2
Output: out
Create 2 EqvClasses separately
E1 (a_1, 3 * in2_1)
E2 (a_2, in1_2 * in2_2)
Check their equivalence … nonequivalent
Identify the statements affected by a_1 or a_2
 5th line is identified
208
An example of verification
a_1 = 3 * in2_1;
b_1 = 360 + in1_1;
c_1 = 2408 * (in1_1 + in2_1);
d_1 = c_1 – 4017 * b_1;
e_1 = 1108 * (a_1 + b_1);
out_1 = (d_1 + e_1) >> 8;

D
E
E
E
E
E
a_2 = in1_2 * in2_2;
b_2 = 360 + in1_2;
c_2 = 2408 * (in1_2 + in2_2);
d_2 = c_2 – 4017 * b_2;
e_2 = 1108 * (a_2 + b_2);
out_2 = (d_2 + e_2) >> 8;
2nd, 3rd, 4th line: textually equivalent and not
affected by nonequivalent variables


These pairs are clearly equivalent  can skip
checking
Simply create an EqvClass for each pair
E3 (b_1, b_2, 360 + in1_1, 360 + in1_2)
E4 (c_1, c_2, 2408 * (in1_1 + in2_1),
2408 * (in2_1 + in2_2))
E5 (d_1, d_2, c_1 – 4017 * b_1, c_2 – 4017 * b_2)
209
An example of verification
a_1 = 3 * in2_1;
b_1 = 360 + in1_1;
c_1 = 2408 * (in1_1 + in2_1);
d_1 = c_1 – 4017 * b_1;
e_1 = 1108 * (a_1 + b_1);
out_1 = (d_1 + e_1) >> 8;

D
E
E
E
E
E
a_2 = in1_2 * in2_2;
b_2 = 360 + in1_2;
c_2 = 2408 * (in1_2 + in2_2);
d_2 = c_2 – 4017 * b_2;
e_2 = 1108 * (a_2 + b_2);
out_2 = (d_2 + e_2) >> 8;
5th line: affected by nonequivalent variable a_1
and a_2



Create 2 EqvClasses separately
E6 (e_1, 1108 * (a_1 + b_1))
E7 (e_2, 1108 * (a_2 + b_2))
Check their equivalence … nonequivalent
Identify the statements affected by e_1 or e_2
 6th line is identified
210
An example of verification
a_1 = 3 * in2_1;
b_1 = 360 + in1_1;
c_1 = 2408 * (in1_1 + in2_1);
d_1 = c_1 – 4017 * b_1;
e_1 = 1108 * (a_1 + b_1);
out_1 = (d_1 + e_1) >> 8;

D
E
E
E
E
E
a_2 = in1_2 * in2_2;
b_2 = 360 + in1_2;
c_2 = 2408 * (in1_2 + in2_2);
d_2 = c_2 – 4017 * b_2;
e_2 = 1108 * (a_2 + b_2);
out_2 = (d_2 + e_2) >> 8;
6th line: textually equivalent, but affected by
nonequivalent variables e_1 and e_2



Create 2 EqvClasses separately
E8 (out_1, (d_1 + e_1) >> 8)
E9 (out_2, (d_2 + e_2) >> 8)
Check their equivalence … nonequivalent
Terminate with the results “nonequivalent”
211
Experiments (MPEG4)

Optimization of IDCT functions (idct_row
& idct_col) in MPEG4

Sizes
 Whole MPEG4 program … more than 17k lines
 Target IDCT functions … about 50 lines

Note
 9 lines are different between descriptions (of
each function)
 Each function has 8 conditional branches (i.e. 256
execution paths have to be proved)
 functions were unrolled 8 times
212
Experiments (MPEG4)
An example of different parts (below)
 Results

 Each pair of functions was proved to be
equivalent
 idct_row … 680 sec
 idct_col … 2190 sec
tmp = x6;
x6 = W3 * x7 + W5 * tmp;
x7 = W3 * tmp – W5 * x7;
x8 = x0 + x1;
Description 1
x8
x6
x7
x8
Optimization
=
=
=
=
W3 * (x6 + x7);
x8 – (W3 – W5) * x6;
x8 – (W3 + W5) * x7;
x0 + x1;
Desciption 2
213
Experiments (AES)

Changes in AES (American Encryption
Standard)

Target: Encryption function in Rijndael
 Rijndael is an implementation of AES


Size: 120 lines
Case 1 (equivalent changes)
 4 different parts were inserted
 Result … equivalent, Verification time … 6 sec

Case 2 (not equivalent changes)
 8 different parts were inserted
 Result … not equivalent, Verification time … 344 sec

Case 2 took longer time because many statements
were affected by nonequivalent variables
214
Synchronization verification: Overview

In system-level design…



Communication among parallel processes is
necessary
To operate properly, those parallel processes must
be correctly scheduled/synchronized
Synchronization verification



Guarantee the order of execution of statements as
designers’ intended
Problem size can be significantly reduced (focus on
some, not all, parts of the design)
More confident when “SV” and “property checking”
than “property checking” alone
215
Par statement in SpecC
C Language
void A() {
A
SpecC Language
void A() {
A
}
void B() {
B
}
void B() {
B
}
void C() {
}
void main() {
A();
B();
C();
}
}
void C() {
C
}
void main() {
par{
A.main();
B.main();
}
C.main();
}
C
216
Synchronization in SpecC

Add notify/wait of event e for sync.

‘wait’ will stop process until it is ‘notify’
void A() {
A
notify e1;
wait e2;
B
Process B stops
and wait until
e1 is notified
}
void B() {
wait e1;
notify e2;
}
void main() {
par {
A.main();
B.main();
}
}
notify e1
Process A stops
and wait until
e2 is notified
A resumes
wait e2
wait e1
notify e2
B resumes
217
Synchronization in SpecC
a.main()
Synchronization by
St1 Notify/wait
St2
main()
main() {{
par{
par{ a.main();
a.main();
b.main();
b.main();}}}}
behavior a {
behavior
main() a
{ {
x=10;
main() {y=x+10;
x=10;
y=x+10;
notify
e;
behavior
behavior bb {{
main()
e;
main() {{ wait
x=20;
x=20;
a.main()
St2
St1
b.main()
St3
b.main()
/*st1*/
/*st1*/
/*st2*/
/*st2*/ }}
/*New*/}}
St3
Tas T1s
/*New*/
/*st3*/ }}
/*st3*/ }}
Tas T1s
Tbs
Ambiguous results on y causing from
x = 10; /*st1*/
x = 20; /*st3*/
Tbs
T1e T2s
T1e T2s
T3s
time
time
T2e Tae
T2e
T3e
T3s
y = 20 (always)
Tae
Tbe
T3e Tbe
218
Synchronization in SpecC (cont.)
Synchronization by
Notify/wait
a.main()
St2
main() {
par{ a.main();
b.main(); }}
St1
behavior a {
main() { x=10;
y=x+10;
notify e;
/*st1*/
/*st2*/
/*New*/}}
behavior b {
main() { wait e;
x=20;
/*New*/
/*st3*/ }}
b.main()
St3
Tas T1s
T1e T2s
Tbs

Tas=Tbs, Tae=Tbe
 Tas<=T1s<T1e<=T2s<T2e<=Tas
 Tbs<=T3s<T3e<=Tbe
 T2e<=T3s
y = 20 (always)
T2e
T3s
time
Tae
T3e Tbe
Synchronization verification for two
concurrent processes (1)

219
Check if wait/notify can acutually
communicate in while loops (or nested loops)

First approach: Delete while loop
 In each iteration notify/wait must communicate
while (1) {
if stmnt
switch stmnt
notify e1
while (1) {
if stmnt
switch stmnt
wait e1
while (1) {
if stmnt
switch stmnt
notify e1
notify e2
wait e1
notify e2
wait e2
wait e2
}
while (1) {
if stmnt
switch stmnt
}
}
}
Synchronization verification for two
concurrent processes (2)

220
Unfold by N and M times

N is 1 to n, M is 1 to m, any combinations
while (1) {
if stmnt
switch stmnt
wait e1
notify e2
while (1) {
if stmnt
switch stmnt
notify e1
while (1) {
if stmnt
switch stmnt
wait e1
notify e2
wait e2
while (1) {
if stmnt
switch stmnt
notify e1
wait e2
}
while (1) {
if stmnt
switch stmnt
notify e1
wait e2
}
}
}
}
while (1) {
if stmnt
switch stmnt
wait e1
notify e2
}
while (1) {
if stmnt
switch stmnt
wait e1
notify e2
}
Synchronization verification for two
concurrent processes (3)

221
While loops are converted into FSM (nested
loops can be treated in the same way)

Basically need regular model checking
while (1) {
if stmnt
switch stmnt
notify e1
while (1) {
if stmnt
switch stmnt
wait e1
notify e2
wait e2
}
if stmnt
notify e1
switch stmnt
wait e2
}
switch stmnt
wait e1
notify e2
if stmnt
222
Example(1)

Par
notify e1
a
wait e2
c
notify e2
behavior1 {notify e1; a; wait e2; b} wait e1
Behavior2 {wait e1; c; notify e2; d}
 e1 < a, a < e2, e2 < b, e1 < c, c < e2, e2 < d
 a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, so the
description is correct

Par
wait e2
a
notify e1
b
d
b
c
notify e2
d
behavior1 {wait e2; a; notify e1; b} wait e1
Behavior2 {wait e1; c; notify e2; d}
 e2 < a, a < e1, e1 < b, e1 < c, c < e2, e2 < d
 a, b, c, d, e1, e2 > 0 are satisfied ? → No, since a < c
and c < a. This means a deadlock !
223
Example(2)

Par
notify e1
a
wait e1
ｗaitfor(10)
ｗaitfor(10)
c
wait e2
b
notify e2
d
behavior1 {notify e1; a; waitfor(10); wait e2; b}
Behavior2 {wait e1; waitfor(10); c; notify e2; d}
 e1 < a, a + 10 < e2, e2 < b, e1 + 10 < c, c < e2, e2 < d
 a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, the design is correct
 Moreover, b<c is satisfied ? → No, the result says c<b

Par
notify e1
a
wait e2
wait e1
ｗaitfor(10)
c
ｗaitfor(10)
b
notify e2
d
behavior1 {notify e1; a; wait e2; waitfor(10); b}
Behavior2 {wait e1; waitfor(10); c; notify e2; d}
 e1 < a, a < e2, e2 + 10 < b, e1 + 10 < c, c < e2, e2 < d
 a, b, c, d, e1, e2 > 0 are satisfied ? → Yes, the design is correct
 Moreover, b – e1 < 20 is satisfied ? → No, this is not satisfied
224
Verification flows

Goals:
Check whether given SpecC codes (with
‘par’, ‘notify/wait’) are properly synchronized
 If checking fails, counter-examples should
be generated (trace to source of errors)


Based on:

Boolean SpecC, a little theorem prover,
SVC/CVC, Program Slicing, ...
225
Verification Flows
Refining
SpecC
behavior A(out event e,
inout int x,
inout int y)
{
void main(){
if (x > 1) {
notify e;
y = x - 1;
}
if (y > 3) {
.
.
Boolean SpecC
Abstraction
behavior A() {
void main(){
if (C0) {
notify e
...
}
if (C1) {
.
.
Correct
Verify
with a theorem
prover
Abstraction refinement
Error-trace
226
Boolean Program
Proposed by Ball and Rajamani under
SLAM project at Microsoft Research
 Think of SW like a model (like FSM in
HW) and verify it by first abstracting
away unnecessary statements with userdefined predicates
 BP abstracts the original program:
if properties on BP hold, so as original
one

227
Our Boolean SpecC
is a subset of original SpecC program
 ‘if-else’ conditions are replaced by
propositional vars. e.g. if(x<y) -> if(c0)
 Statements other than ‘notify/wait’ and
‘if’, (ones that don’t effect the sync.) are
abstracted away (abstract unnecessary
info.)
 Only for verification of synchronization

228
Abstraction refinement
Refining
SpecC
Boolean SpecC
behavior A(out event e,
inout int x,
inout int y)
{
void main(){
if (x > 1) {
notify e;
y = x - 1;
}
if (y > 3) {
.
.
Abstraction
behavior A() {
void main(){
if (C0) {
notify e
...
}
if (C1) {
.
.
Correct
Verify
with a theorem
prover
Error-trace
Constructing Control
Flow Graph (CFG)
Entry barber
while
numCustomer
if numCustomer = 0
DayDreaming
KeepCutting
chairOccupied
call
if numCustomer != 0
if chairOccupied = T
chairOccupied = F
Find & Modify
Predicates
if chairOccupied = F
notify call
chairOccupied = T
Abstraction refinement
Check validity
Symbolic sim
& theorem prover
229
Abstraction refinement
1.
2.
3.
SpecC => boolean SpecC & build
Control Flow Graph (CFG)
Verify with theorem provers. If result is
satisfied, terminate, else go to next step
Use CFG to find related path and
symbolically simulate along the path


4.
5.
Use theorem provers on the validity of the path
If not a feasible path, analyze and generate
conditions on Boolean program variables using
SpecC program slicing
Use those conditions and modify boolean
SpecC
Go to 2
230
Example: Sleeping barber problem
barber
customer
empty chair
•
•
•
•
•
barber chair
barber: finished cutting->call customer
barber: no customer->wait
customer: barber wait->has hair cut
customer: chairs occupied->come again
customer: a chair empty->wait
par statement
barber
customer
if no-customer
T
Day dreaming
if no-customer
F
F
Cutting
Go back
T
Enter barber
F
if finish cut
Wait for ‘Call’
T
‘Call’ next customer
Sit & had a hair cut
Customer leave
Leave
231
Example
behavior Main () {
void main() {
par {
barber.main();
customer.main();
}
}
};
behavior barber (inout event call,
inout bool chairOccupied,
inout bool waitCustomer) {
void main() {
behavior customer (inout event call,
inout bool chairOccupied,
inout bool waitCustomer) {
void main() {
while(1) {
while(1) {
if (waitCustomer == false)
if (waitCustomer == false)
DayDreaming();
waitCustomer = true;
else {
else {
if (chairOccupied == true) {
waitCustomer = false
KeepCutting();
if (chairOccupied == false)
chairOccupied = false;
wait call;
}
}
else {
notify call;
chairOccupied = true;
};
}
}
};
232
Abstract
/* Barber */
/* Barber */
void main() {
void main() {
while(1) {
while(a0) {
if (!waitCustomer)
DayDreaming();
if (a1)
(A1)
...
else {
else {
if (chairOccupied) {
if (a2) {
KeepCutting();
(A2)
...
chairOccupied = false;
(A3)
...
Construct model + Verify
}
}
else {
else {
notify call;
(A4)
notify call;
chairOccupied = true;
(A5)
...
}
}
};
};
/* Customer */
/* Customer */
void main() {
void main() {
while(1) {
while(b0) {
if (!waitCustomer)
waitCustomer = true;
if (b1)
(B1)
...
else {
waitCustomer = false;
else {
(B2)
...
if (!chairOccupied)
wait call;
if (b2)
(B3)
wait call;
}
};
}
};
Property to be verified:
‘notify’ is not reached,
‘wait’ is reached, then
Synchronization error!

A4 is not reached
and
B3 is reached

Error!!! (Deadlock)
a2

chairOccupied==true
a1

waitCustomer==false
233
/* Barber */
/* Barber */
/* Barber */
/* Barber */
void main() {
void main() {
void main() {
void main() {
while(1) {
while(1) {
while(1) {
while(1) {
if (!waitCustomer)
if (a1)
if (a1)
if (a1)
DayDreaming();
...
...
...
else {
else {
if (chairOccupied) {
else {
if (a2) {
else {
if (a2) {
if (a2) {
KeepCutting();
...
...
...
chairOccupied = false;
...
!a2
!a2
}
}
}
}
else {
else {
else {
else {
notify call;
notify call;
notify call;
notify call;
chairOccupied = true;
...
a2
a2
}
}
}
}
};
};
};
};
/* Customer */
/* Customer */
/* Customer */
/* Customer */
void main() {
void main() {
void main() {
void main() {
while(1) {
while(1) {
if (!waitCustomer)
if (b1)
if (a1)
...
...
!a1
else {
else {
else {
waitCustomer = false;
...
...
a1
if (!chairOccupied)
if (b2)
if (!a2)
if (!a2)
wait call;
wait call;
}
};
while(1) {
if (b1)
waitCustomer = true;
else {
while(1) {
}
};

wait call;
}
};

wait call;
}
};

Evaluation of the synchronization
verification methods(1)
We injected ‘wait’ statements into the
original SpecC descriptions (to cause
deadlock, and verify it)
 Focusing only synchronization
(notify/wait under par{ }), problem size
can be significantly reduced
 Running on Linux machine, P3 1.1GHz &
2GB RAM, deadlock can be detected
within few minutes

234
235
How to deal with loops ?

Loops that create numbers of ‘notify/wait’ have
to be unwound to get the equal numbers of
notify and wait (analysis on loops of
‘notify/wait’ can be considered as another
interesting research topic)
This loop creates infinite numbers of notify(clk16)
behavior gen_clk16() {
void main() {
while(1) {
waitfor(10);
notify(clk16);
}
}
};
This loop creates infinite numbers of wait(clk16)
With multiple of 16 ‘wait(clk16)’ each time
behavior tx_clk() {
void main() {
while(1) {
for(i = 0; i < 16; i++)
wait(clk16);
notify(bit_event);
}
}
};
236
Experimental results

FIFO example



Point-to-point protocol



~850 lines
5 behaviors have sync. semantic, 12 behaviors total
Elevator control system



~260 lines
3 behaviors and 2 interfaces
~2000 lines
3 behaviors have sync. semantic, 13 behaviors total
MPEG4


~48,000 lines
3 behaviors have sync. semantic, XX behaviors total
237
Experimental results
Properties: checking for deadlock
# of lines
O riginal Sync.V er.
V erification Tim e (seconds)
P roperty1
P roperty2
P roperty3
FIFO
260
240
3.83
3.89
3.85
P oint-to-P oint P rotocol
850
500
12.34
12.42
13.2
Elevator C ontrolSystem
2000
800
30.67
29.82
29.9
M P EG 4
48000
800
27.79
27.66
28.11
When consider only parallel behaviors
Problem size (# of lines) can be reduced
238
C Bounded Model Checking


CBMC

Developed at CMU, 2003

[1] Hardware Verification using ANSI-C Programs as a Reference
(Proc. of ASPDAC’03)
Characteristics



Modeling … C program -> Bit vector equation
Specifying properties … inserting assertions in C
programs
C program
Verification … using SAT solver
Modeling
Bit Vector Equation
Specifying properties
Verification
using SAT solver
Result
239
What does CBMC do?

CBMC checks if or not C programs satisfy the
properties the user specify


Input … C Program with assertions as properties
Output … Result (Success/Fail). If fails, a counter
example is reported
char a, b;
int c;
if (a < b) c = b – a;
else c = a – b;
assert (c >= 0);
char a, b;
int c;
if (a < b) c = b – a;
else c = a – b;
assert (c != 0);
Success
Fail
Counter example (a = 39, b = 39)
240
Bounded Model Checking (BMC)

A kind of Model Checking techniques



Checking whether the design satisfies the property
up to certain finite numbers of execution cycles
(bound) on the system
Correctness of the design is guaranteed only up to
the bound
BMC is useful when the design is too large to
handle for other formal methods

BMC can detect many bugs although it only
guarantees that there is no counter examples up to
the bound number of execution cycles
241
BMC for C Programs

What does “bound” mean in C program?


Input
In C programs, cycle is not explicit
“bound” means the number of loop unwinding
Combinational circuit
Combinational circuit
Combinational circuit
Output Satisfies given
properties?
BMC in RTL (behavior of
only 3 cycles are verified)
Loop
Unwinding
Loop
Loop
BMC of a loop in C program
Loop
242
Process of CBMC
x  x  y;
if ( x! 1) x  2;
else x  ;
assert( x  3);
C : ( x1  x0  y0 ) 
( x2  ((x1  1) ? 2 : x1 )) 
Modeling
Given C program
& properties
( x3  ((x1  1) ? x2  1 : x2 )
P : x3  3
Bit vector equation
Generating SAT formula
Result (success/fail)
counter example
SAT solver
(Chaff)
243
Transforming ANSI-C (1)

Renaming



v  v
After renaming, each variable appears only once in
the left hand side of assignments
α is the number of assignments made to variable v
x1  x0  y0 ;
x  x  y;
if ( x! 1) x  2;
else x  ;
if ( x1! 1) x2  2;
assert( x  3);
assert( x3  3);
else x3  x2  1;
244
Renaming
x  x  y;
if ( x! 1) x  2;
else x  ;
assert( x  3);
x1  x0  y0 ;
if ( x1! 1) x2  2;
else x3  x2  1;
assert( x3  3);
x  x  y;  x1  x0  y0 ;
x, y in right hand are not assigned yet
x in left hand is assigned at the 1st time
if ( x! 1)  if ( x1! 1)
This x is equivalent to
the x after the 1st assignment
x  2;  x2  2;
This x is assigned at the 2nd time
・・・
245
Transforming ANSI-C (2)

Transformation into bit vector equation



Formula C describes the Constraint of the
verification
Formula P describes the Property to be verified
Checking if or not “C -> P” is always true
x1  x0  y0 ;
if ( x1! 1) x2  2;
else x3  x2  1;
assert( x3  3);
C : ( x1  x0  y0 ) 
( x2  ((x1  1) ? 2 : x1 )) 
( x3  ((x1  1) ? x2  1 : x2 )
P : x3  3
Formal definition of transformation from
C into bit vector equation
x1  x0  y0 ;
if ( x1! 1) x2  2;
else x3  x2  1;
assert( x3  3);

C : ( x1  x0  y0 ) 
( x2  ((x1  1) ? 2 : x1 )) 
( x3  ((x1  1) ? x2  1 : x2 )
P : x3  3
C(p, g) and P(p, g)
C(p,g) computes the assignments
 P(p,g) computes the properties

 p … program block
 g … guard (condition that p is operated)
246
247
Example of transformation
x1  x0  y0 ;
if ( x1! 1) x2  2;
else x3  x2  1;
S … assignment
S’ … conditional branch
assert( x3  3);
If the program is a sequential
composition, C (p, g) is split by
using ∧ operator
Apply this rule
C  C (S ; S ' , true)  C (S , true)  C (S ' , true)
※At the start of the program,
“guard” is always “true”
248
Example of transformation
x1  x0  y0 ;
S … assignment
if ( x1! 1) x2  2;
else x3  x2  1;
S’ … conditional branch
assert( x3  3);
If program is an assignment v = e,
C (p, g) is generally described as
C(v  e, g ) : v  g ? e : v 1
Apply this rule
C  C ( S , true)  C ( S ' , true)
 ( x1  x0  y0 )  C ( I , true)
249
Example of transformation
x1  x0  y0 ;
S … assignment
if ( x1! 1) x2  2;
S’ … conditional branch
else x3  x2  1;
assert( x3  3);
If program is a conditional branch if(c) I; else I’;,
C (p, g) is generally described as
C (if (c) I
else I , g ) : C ( I , g  c)  C ( I , g  c)
Apply this rule
C  ( x1  x0  y0 )  C ( S ' , true)
 ( x1  x0  y0 )  C ( x2  2, x1  1)  C ( x3  x2  1, x1  1)
 ( x1  x0  y0 )  ( x2  ( x1  1) ? 2 : x1 )  ( x3  ( x1  1) ? x2  1 : x2 )
250
Example of transformation
x1  x0  y0 ;
if ( x1! 1) x2  2;
else x3  x2  1;
Assertion
assert( x3  3);
Computation of P formula from assertions
P(assert(a), g ) : g  a
Apply this rule
P  ( x3  3)
※ In this case, guard is true
251
Loop unwinding

CBMC makes loops unwind finite times

Because “Bounded” Model Checking
 Only the finite number of statements are verified


The number of unwinding can be determined by
the user
Unwinding process

Do loop unwinding n times by the following
transformation
while (e) inst; → if (e) { inst; while (e) inst; }


The last while loop is replaced by assert(!e);
(“unwinding assertion”)
If “unwinding assertion” is satisfied, the number
of unwinding is sufficient
252
Unwinding assertion
while (e)
inst;
Unwinding
n times
Original loop
Verification
Is “unwinding
assertion” violated?
no
yes
Need to unwind
more
if (e) {
inst;
if (e) {
inst;
if (e) {
inst;
assert(!e);
}
}
}
Unwinding is Unwound loop
sufficient
unwinding
assertion
253
Removing pointers

Pointer dereferences are removed in the
process of transformation
 Example.
if (x) p = &a;
else p = &b;
*p =1;
x = true -> *p = a
x = false -> *p = b
What does this pointer dereference?
How do we remove pointers automatically?
Introducing the φ function
to analyze pointer dereferences
Removing pointers by using the φ
function

Definition
* e   (e, g ,0)



e[o]   (e, g , o)
e … sub-expression to be dereferenced
g … guard (condition that the dereference is
operated)
o … offset
if ( x0 ) p1  &a0 ;
if ( x) p  &a;
else p  &b;
else p2  &b0 ;
Renaming
* p  1;
* p2  1;
* p2
  ( p2 , true,0)  ...(many processes)...  x0 ? a0 : b0
254
255
Verification with SAT Solver

Satisfiability Problem (SAT Problem)



Formula F is satisfiable if there is more than one
input pattern that makes F true
Ex. F1 = a ∧ b … satisfiable (when a = true, b = true)
Ex. F2 = a ∧ ￢a … not satisfiable
C : ( x1  x0  y0 ) 
x2  ((x1  1) ? 2 : x1 ) 
x3 
If (C -> P) is always true,
￢（C -> P） is not satisfiable
((x1  1  z0 ) ? x2  1 : x2 )
P : x3  3
Bit vector equation from
C program
Verification with SAT solver
(Chaff)
256
Checking over bound access to array
int exam () {
int array[3], i, sum=0;
for (i=0; i<=3; i++) {
array[i] = input();
sum = sum + array[i];
}
return sum;
}

CBMC can detect the over bound access to
array indices


This means the value
is input at this point
This program is faulty since array[3] is accessed
when i = 3
If (i <= 3) is replaced by (i < 3), this program
becomes correct
257
Assertion checking
int main () {
unsigned char a, b;
unsigned char ai, bi;
unsigned int result = 0, i;
a = input;
b = input;
for (i = 0; i < 8; i++) {
bi = (b>>i);
ai = (a<<i);
if ( bi & 1)
result += ai;
}
assert (result == a * b);
}

CBMC can verify datadominant properties

<-> control-dominant
properties as “safety
properties”
Suppose i=1
101 (a)
× 1010 (b)
bi = 1
ai = 10100
This corresponds to
the sub-product of
(a) * (2nd digit of b)
258
Experimental results

Using CBMC, the behavioral consistency of C
and Verilog programs can be checked
Behavioral consistent?
Verilog

C
Some experimental results are reported below*

PS/2 interface
 700 lines of Verilog, unwinding bound 48, run time 51 sec.

DLX processor
 Verilog design with 1219 latches, 550 lines of C, run time 97
sec., detected a counter example of length 5 cycles
*: Behavioral Consistency of C and Verilog
Using Bounded Model Checking (Proc. of DAC’03)
259
Final remarks: Verification directions

Driven by design flow

Higher levels of abstraction
 Formal specification languages
 Mapping verification problems to lower level engines

Design reuse
 Interface verification
 System level verification

Tackling larger designs in formal verification



Efficient formal engines
Sequential equivalence checkers
Filter based techniques
 Using multiple engines

Hybrid engines
 E.g. BDD/SAT/ATPG combination

Higher level reasoning
 Need to automate
260
Final remarks: Research issues

Design and verification at high levels of abstraction


New modeling issues
Eg: what if Spec is in UML
 How to generate problem, map problem

Faster engines

More efficient BDDs
 Efficient and automatic abstraction-refinement

Faster SAT solvers
 Better learning and pruning techniques

Combining engines
 ATPG/SAT combination
 BDD/SAT combination



Use of higher level information to guide search
Methodology issues
Interface specification and verification

Automatic static checks
261
Bibliography on verification
262
Books














B. Berard et. al., “Systems and Software Verification: Model Checking Techniques and
Tools”, Springer Verlag, 2001.
J. Bergeron, “Writing Testbenches: Functional Verification of HDL Models”, Kluwer
Academic Publishers, Boston, 2000.
D.D. Gajski et. al., “SpecC: Specification Language and Methodology”, Kluwer
Academic Publishers, Boston, 2000.
J. Bhasker, “ A SystemC Primer ”, Star Galaxy Press, Allentown, 2002.
M. Suart and D. Dempster, “ Verification Methodology Manual for Code Coverage in
HDL Designs”, Teamwork International, Hampshire, UK, 2000.
K. L. McMillan, ``Symbolic Model Checking'', Kluwer Academic Publishers, 1993.
Z. Manna and A. Pnueli, “Temporal Specification and Verification of Reactive
Systems” Vol. I and II, Springer 1995.
Ching-Tsun Chou, "The Mathematical Foundation of Symbolic Trajectory Evaluation",
Springer-Verlag 1999.
Thomas Kropf: "Introduction to Formal Hardware Verification", (Springer Verlag;
ISBN: 3540654453, 299 pages, January 2000)
E. M. Clarke, O. Grumberg and D. Peled, "Model Checking", (MIT Press; ISBN:
0262032708; 330 pages; January 2000)
G. J. Holzmann, “Design and Validation of Computer Protocols”, Prentice Hall, 1991.
M. P. Fourman, “Formal System Design”, Formal Methods for VLSI Design, IFIP, 1990,
North-Holland.
C. Meinel and T. Theobald, “Algorithms and Data Structures in VLSI Design”,
Springer-Verlag, 1998.
Hassan Gomaa, “Designing Concurrent, Distributed and Real-Time Applications with
UML”, Addison-Wesley, July 2000.
263
Books













L. Bening and H. Foster, “Principles of Verifiable RTL Design: Functional Coding Style
Supporting Verification Processes in Verilog”, published by Kluwer Academic Publishers, 2000.
R. P. Kurshan, “Computer Aided Verification of Coordinating Processes”, Princeton University
Press, 1994.
Robert B. Jones, “Symbolic Simulation Methods for Industrial Formal Verification”, Kluwer
Academic Publishers, Boston, 2002.
M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991. (Book
containing a collection of papers)
R. P. Kurshan, “Computer Aided Verification of Coordinating Processes”, Princeton University
Press, 1994.
G. J. Holzmann, “Design and Validation of Computer Protocols”, Prentice Hall, 1991.
M. P. Fourman, “Formal System Design”, Formal Methods for VLSI Design, IFIP, 1990, NorthHolland.
C. Meinel and T. Theobald, “Algorithms and Data Structures in VLSI Design”, Springer-Verlag,
1998.
M. Kaufmann, P. Manolios, and J S. Moore, "Computer-Aided Reasoning: An Approach",
(Kluwer Academic Publishers, June 2000; ISBN 0792377443)
Robert B. Jones, Symbolic Simulation Methods for Industrial Formal Verification, Kluwer
Academic Publishers, Boston, 2002.
M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991. (Book
containing a collection of papers)
M. Kaufmann, P. Manolios, and J S. Moore, "Computer-Aided Reasoning: An Approach",
(Kluwer Academic Publishers, June 2000; ISBN 0792377443)
M. Keating and P. Bricaud “Reuse Methodology Manual for System-On-A-Chip Designs,” Kluwer
Academic Publishers, June 1998.
264
Papers
High Level Design and Verification Modeling






D. D. Gajski, ``IP-Based Design Methodology'', Proc. of the 36th Design Automation
Conference, pp. 43, New Orleans, June 1999.
D. Kroening and E. Clarke, “Behavioral consistency of C and Verilog programs using
bounded model checking,” in Proc. DAC, June 2003.
T. Sakunkonchak and M. Fujita, “Verification of synchronization in SpecC description with
the use of difference decision diagram,” IEICE Trans. Fundamentals, Vol. E85-A, Jan 2002.
T. Matsumoto and M. Fujita, “Equivalence checking of C-based hardware descriptions by
using symbolic simulation and program slicer,” in Proc. IWLS, May 2003.
T. Ball and S. Rajamani, “Checking Temporal Properties of Software with Boolean
Programs”, in Proc. Computer Aided Verification 2000, [Microsoft SLAM project]
R. Bryant et . al. “Processor Verification Using Efficient Reductions of the Logic of
Uninterpreted Functions to Propositional Logic” in ACM Trans. on Computational Logic,
Vol 2., 2001.

S. Singh, “Design and Verification of CoreConnectTM IP using Esterel,” in Proc CHARME
2003

S. Sutherland, “System Verilog 3.1 Its what the DAVEs in you company asked for”. in Proc.
DVCON 2003

S. Abdi, D. Shin and D. Gajski, "Automatic Communication Refinement for System Level
Design,” Proceedings of Design Automation Conference, Anaheim, CA, June 2003.

W. Mueller, R. Dömer, A. Gerstlauer, "The Formal Execution Semantics of SpecC,"
in Proceedings of International Symposium on System Synthesis, October 2002.
265
Papers
Theorem Proving & Decision Procedures










S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS:
Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96.
S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS:
Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96.
D. Cyrluk, S. Rajan, N. Shankar and M. K. Srivas, “Effective Theorem Proving for
Hardware Verification”, pp. 287-305, TPCD94.
S. J. Garland and J. V. Guttag, “An Overview of LP: the Larch Prover”, Proceedings of
the Third International Conference on Rewriting Techniques and Applications, 1989,
Springer-Verlag.
J. Staunstrup and M. Greenstreet, “Synchronized Transitions”, Formal Methods for
VLSI Design, 1990, IFIP, North-Holland.
R. Vemuri, “How to Prove the Completeness of a Set of Register Level Design
Transformations”, Proceedings of the 27th ACM/IEEE Design Automation Conference,
1990, 207—212.
D. Cyrluk, S. Rajan, N. Shankar and M. K. Srivas, “Effective Theorem Proving for
Hardware Verification”, pp. 287-305, TPCD94.
S. J. Garland and J. V. Guttag, “An Overview of LP: the Larch Prover”, Proceedings of
the Third International Conference on Rewriting Techniques and Applications, 1989,
Springer-Verlag.
J. Staunstrup and M. Greenstreet, “Synchronized Transitions”, Formal Methods for
VLSI Design, 1990, IFIP, North-Holland.
C. M. Angelo, “Formal Hardware Verification ina Silicon Compilation Environment by
means of Theorem Proving”, Ph.D. Dissertation, Katholieke Universiteit Leuven
(February, 1994).
266
Papers









R. Vemuri, “How to Prove the Completeness of a Set of Register Level Design
Transformations”, Proceedings of the 27th ACM/IEEE Design Automation Conference,
1990, 207—212.
Jeffrey J. Joyce and Carl-Johan H. Seger, “Linking Bdd Based Symbolic Evaluation to
Interactive Theorem Proving”, Proceedings of the 30th Design Automation
Conference, 1993.
S. P. Rajan, N. Shankar and M. Srivas, “An Integration of Model-Checking with
Automated Proof Checking”, 7th Conference on Computer-Aided Verification, July,
1995.
M.D. Aagard, R.B. Jones and C.-J.H. Seger, “Combining Theorem Proving and
Trajectory Evaluation in an Industrial Environment”, Proceedings of DAC 1998, pp.
538-541
C.W. Barrett, D.L. Dill and J.R. Levitt, “A Decision Procedure for Bit-Vector
Arithmetic”, Proceedings of DAC 1998
J.R. Burch and D.L. Dill, “Automatic Verification of Pipelined Microprocessor
Control”, Proceedings of CAV 1994
J.X. Su, D.L. Dill and C.W. Barrett, “Automatic Generation of Invariants in Processor
Verification”, Proceedings of FMCAD 1996
M. Aagaard, M. E. Leeser, and P. J. Windley, “Toward a Super Duper Hardware Tactic”,
in Higher Order Logic Theorem Proving and its Applications: 6th International
Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J.
Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (SpringerVerlag, 1994), pp. 399-412.
F. Andersen, K. D. Petersen, and J. S. Pettersson, `A Graphical Tool for Proving UNITY
Progress', in Higher Order Logic Theorem Proving and Its Applications: 7th
International Workshop, Valletta, Malta, September 1994: Proceedings, edited by T. F.
Melham and J. Camilleri, Lecture Notes in Computer Science, Volume 859 (SpringerVerlag, 1994), pp. 17-32.
267
Papers








S. Agerholm, `Domain Theory in HOL', in Higher Order Logic Theorem Proving and its
Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13
1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in
Computer Science, vol. 780 (Springer-Verlag, 1994), pp. 295-310.
S. Agerholm, `Formalising a Model of the lambda-calculus in HOL-ST' Technical
Report Number 354, University of Cambridge Computer Laboratory (1994).
S. Agerholm, “A HOL Basis for Reasoning about Functional Programs”, Ph.D.
Dissertation, BRICS Technical Report RS-94-44, Department of Computer Science,
University of Aarhus (December 1994).
S. Agerholm, “LCF Examples in HOL”, The Computer Journal, vol. 38, no. 2 (July
1995), pp. 121-130.
S. Agerholm, `Mechanizing Program Verification in HOL', in Proceedings of the 1991
International Workshop on the HOL Theorem Proving System and its Applications,
Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley
(IEEE Computer Society Press, 1992), pp. 208-222.
S. Agerholm, `Mechanizing Program Verification in HOL', M.Sc. Dissertation, DAIMI
Report Number IR-111, Department of Computer Science, University of Aarhus (April
1992).
S. Agerholm “Non-Primitive Recursion Function Definition”, in Higher Order Logic
Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove,
Utah, September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley, and J.
Alves-Foss, Lecture Notes in Computer Science, Volume 971 (Springer-Verlag, 1995),
pp. 17-31.
F. Andersen and K. D. Petersen, `Recursive Boolean Functions in HOL', in
Proceedings of the 1991 International Workshop on the HOL Theorem Proving
System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K.
N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992), pp. 367-377.
Papers







C. M. Angelo, L. Claesen, and H. De Man, “Degrees of Formality in Shallow Embedding
Hardware Description Languages in HOL”, in Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, HUG'93, Vancouver, B.C., August 11-13
1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer
Science, vol. 780 (Springer-Verlag, 1994), pp. 89-100.
C. M. Angelo, L. Claesen, and H. De Man, `The Formal Semantics Definition of a MultiRate DSP Specification Language in HOL', in Higher Order Logic Theorem Proving and
its Applications: Proceedings of the IFIP TC10/WG10.2 International Workshop, Leuven,
September 1992, edited by L. J. M. Claesen and M. J. C. Gordon, IFIP Transactions A-20
(North-Holland, 1993), pp. 375-394.
C. M. Angelo, L. Claesen, and H. De Man, “Modeling Multi-rate DSP Specifiction
Semantics for Formal Transformational Design in HOL”, Formal Methods in System
Design, vol. 5, nos. 1/2 (July 1994), pp. 61-94.
R. J. R. Back and J. von Wright, `Predicate Transformers and Higher Order Logic', in
Semantics: Foundations and Applications: REX Workshop, Beekbergen, June 1992,
edited by J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Lecture Notes in
Computer Science, Volume 666 (Springer-Verlag, 1993), pp. 1-20.
R. J. R. Back and J. von Wright, `Refinement Concepts Formalised in Higher Order
Logic', Formal Aspects of Computing, Vol. 2, No. 3 (July-September 1990), pp. 247-272.
S. Bainbridge, A. Camilleri, and R. Fleming, `Industrial Application of Theorem Proving
to System Level Design', in Proceedings of the 1991 International Workshop on the
HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M.
Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992),
pp. 130-142.
F. Andersen, K. D. Petersen, and J. S. Pettersson, `Program Verification using HOLUNITY', in Higher Order Logic Theorem Proving and its Applications: 6th International
Workshop, HUG'93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J.
Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780 (SpringerVerlag, 1994), pp. 1-15.
268
269
Papers






R. H. Beers and P. J. Windley, `Abstracting Signals: The waveform Library', in
Supplementary Proceedings of the 9th International Conference on Theorem Proving in
Higher Order LogicsL TPHOLs ’96, edited by J. von Wright, J. Grundy, and J. Harrison,
TUCS General Publication No 1, Turku Centre for Computer Science (August, 1996), pp.
1-13.
G. Birtwistle and B. Graham, `Verifying SECD in HOL', in Formal Methods for VLSI
Design: IFIP WG 10.2 Lecture Notes, edited by J. Staunstrup (North-Holland, 1990), pp.
129-177.
G. Birtwistle, B. Graham, and S.-K. Chin, “New theory HOL: An Introduction to Hardware
Verification in Higher Order Logic”, (August 1994). [Published electronically.]
R. Boulton, `Boyer-Moore Automation for the HOL System', in Higher Order Logic
Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2
International Workshop, Leuven, September 1992, edited by L. J. M. Claesen and M. J.
C. Gordon, IFIP Transactions A-20 (North-Holland, 1993), pp. 133-142.
R. Boulton, “Combining Decision Procedures in the HOL System”, in Higher Order
Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove,
Utah, September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley, and J.
Alves-Foss, Lecture Notes in Computer Science, Volume 971 (Springer-Verlag, 1995),
pp. 75-89.
R. J. Boulton, “Efficiency in a Fully-Expansive Theorem Prover”, Ph.D. Dissertation,
Technical Report Number 337, University of Cambridge Computer Laboratory (May
1994).
270
Papers
Formal Verification: SAT Solvers




J. Marques-Silva and K. Sakallah, “GRASP: A Search Algorithm for Propositional
Satisfiability”, IEEE Transactions on Computers, 48(5):506-521, May 1999
M. Sheeran and G. Stalmarck, “A tutorial on Stalmarck’s proof procedure for
propositional logic”, Formal Methods in System Design, 16(1):23-58, January 2000
M.H. Moskewicz et. al., “Chaff: engineering an efficient SAT solver,” in Proc. Design
Automation Conf., June 2001.
E. Goldberg and Y. Novikov, “BerkMin: a Fast and Robust Sat-Solver”, Proceedings of
Design Automation and Test in Europe, pp.142-149, March 2002.
Formal Verification: BDDs






R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE
Transactions on Computers, Vol. C-35-8, pp. 677- 691, August 1986
R. Rudell, “Dynamic Variable Ordering for Ordered Binary Decision Diagrams”,
Proceedings of ICCAD 1993, pp. 42- 45
R. E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations
of Boolean Functions with Application to Integer Multiplication”, IEEE Transactions on
Computers, Vol. 40, No. 2, pp, 205-213, February 1991
B. Bollig and I. Wegener, “Improving the variable ordering for OBDDs is NP-complete”,
IEEE Transactions on Computers, Vol. 45, No. 9, pp. 993-1002, September 1996
M. Fujita, H. Fujitsawa and Y. Matsunaga, “Variable Ordering Algorithms for Ordered
Binary Decision Diagrams and their Evaluation”, IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, Vol. 12, No. 1, pp. 6- 12, January
1993
R. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams”,
slides from a presentation by Prof. Bryant in August 1999
271
Papers
Formal Verification: Symbolic Model Checking (BDDs)










D. L. Dill, “The Mur Verification System”, 390-393, CAV96.
R. Bryant, E. Clarke, K. McMillan and A. Emerson, “Binary Decision Diagrams and
Symbolic Model Checking”, slides from a presentation at Symposium on Algorithms
in the Real World, May, 2000
E. M. Clarke, E. A. Emerson and A. P. Sistla, ``Automatic Verification of Finite-State
Concurrent Systems Using Temporal Logic Specifications'', ACM Trans. on
Programming Language and Systems, Vol.8, No.2, pp 244-263, April 1986.
J. Burch, E. Clarke, D. Long, K. McMillan, D. Dill, “Symbolic Model Checking for
Sequential Circuit Verification”, IEEE Trans. Computer Aided Design, 13, 1994, 401424.
C. Kern and M. Greenstreet, "Formal Verification in Hardware Design: A Survey", ACM
Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193.
H. Iwashita and T. Nakata, `` Forward Model Checking Techniques Oriented to Buggy
Designs'', Proceedings of ICCAD, pp. 400-404, 1997.
K. Takayama, T. Satoh, T. Nakata, and F. Hirose, ``An approach to Verify a Large Scale
System-on-a-chip Using Symbolic Model Checking'', Proceedings of ICCD, 1998.
A. J. Hu, “Formal Hardware Verification with BDDs : An Introduction”, ACM
Transactions on Programming Languages and Systems, 1997.
M. Kaufmann, A. Martin, and C. Pixley, "Design Constraints in Symbolic Model
Checking", Proc. CAV-98, pp. 477-487, 1998.
K. L. McMillan, "Fitting formal methods into the design cycle", Proceedings of the 31st
Design Automation Conference, pp. 314-19, 1994
272
Papers
Formal Verification with SAT solvers







P. Abdulla, P. Bjesse and N. Een, “Symbolic Reachability Analysis Based on SAT
Solvers”, Proceedings of Tools and Algorithms for the Construction and Analysis of
Systems (TACAS), pp. 41-425, March 2000
P. Williams et al, “Combining Decision Diagrams and SAT Procedures for Efficient
Symbolic Model Checking”, Proc. of the 12th CAV, pp. 124-138, July 2000
M. Sheeran, S. Singh and G. Stalmarck, “Checking Safety Properties Using Induction
and a SAT Solver”, Proc. of the 3rd Intl. Conference on Formal Methods in CAD
(FMCAD), pp. 208-125, Nov. 2000
P. Bjesse and K. Claessen, “SAT-based Verification without State Space Traversal”,
Proc. of the 3rd FMCAD, pp. 372-389, Nov. 2000
K.L. McMillan, “Applying SAT Methods in Unbounded Model Checking”, Proc. of the
14th CAV, pp. 250-264, July 2002
K.L. McMillan, “Interpolation and SAT-based Model Checking”, Proc. of the 15th CAV,
July 2003
I. Park and H. Kang, “SAT-based unbounded symbolic model checking”, Proceedings
of DAC, pp. 840-843, June 2003
273
Papers
Equivalence Checking








D. Brand, “Verification of Large Synthesized Designs”, Proceedings of ICCAD,
November 1993, pp. 534-537
A. Kuehlmann and F. Krohm, “Equivalence Checking using Cuts and Heaps”,
Proceedings of DAC 1997, pp. 263-268
Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits”,
Proceedings of DAC 1996, pp. 629-634
R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. Abraham and D. Fussell, “An Efficient
Filter Based Approach for Combinational Verification”, in IEEE Transactions on CAD,
18:1542-1557, Nov. 1999
H. Cho and C. Pixley, “Apparatus and Method for deriving correspondences between
storage elements of a first circuit model and storage elements of a second circuit
model”, U.S. Patent 5,638,381, June 1997
K. Ng, M. Prasad, R. Mukherjee and J. Jain, “Solving the Latch Mapping Problem in an
Industrial Setting”, Proceedings of DAC 2003, pp. 442-447
C.A.J. van Eijk, “Sequential Equivalence Checking Based on Structural Similarities”,
IEEE Transactions on CAD, 19(7):814-819, July 2000
S.-Y. Huang, K.-T. Cheng, K.-C. Chen and F. Brewer, “AQUILA: An Equivalence
Checking System for Large Sequential Circuits”, IEEE Transactions on Computers,
49(5), May 2000
274
Papers
Semi-Formal Verification










R. E. Bryant, “Symbolic Simulation -- Techniques and Applications”, Proceedings of
DAC 1990
R.B. Jones, “Applications of Symbolic Simulation to the Formal Verification of
Microprocessors”, Ph.D. Thesis, Computer Systems Laboratory, Stanford University,
August 1999
R.E. Bryant and C.J.H. Seger, “Formal hardware verification by symbolic trajectory
evaluation,” in Proc. Design Automation Conf., June 1991.
C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of
Partially Ordered Trajectories”, Formal Methods in System Design, Vol. 6, No. 2, pp.
147-190, 1995
E. Clarke, A Biere, R. Raimi and Y. Zhu, “Bounded Model Checking Using Satisfiability
Solving”, in Formal Methods in System Design, 19(1): 7-34, July 2001, Kluwer
Academic Publishers
O. Shtrichman, “Tuning SAT Checkers for bounded model checking,” in Proc. Int.
Conf. on Computer-Aided Verification, July 2000.
F. Fallah, “Binary Time-Frame Expansion”, Proc. of ICCAD, pp. 458-464, Nov. 2002
A. Gupta et al, “Learning from BDDs in SAT-based bounded model checking,” in
Proc. Design Automation Conf., June 2003.
V. Boppana, S. Rajan, K. Takayama and M. Fujita, “Model Checking Based on
Sequential ATPG”, Proceedings of CAV, pp. 418-430, July 1999.
J. Abraham, V. Vedula and D. Saab, “Verifying Properties Using Sequential ATPG”,
Proceedings of International Test Conference, October 2002
275
Papers







D. Dill and S. Tasiran, "Simulation meets Formal Verification?", slides from a
presentation at ICCAD'99.
D. Dill, "Alternative Approaches to Formal Verification (Symbolic Simulation)", slides
from a presentation at CAV 1999.
C. H. Yang and D. L. Dill, “Validation with Guided Search of the State Space”,
Proceedings of DAC 1998
M. Ganai et al, “SIVA: A System for Coverage Directed State Space Search”, In
Journal of Electronic Testing: Theory and Applications (JETTA), February 2001
P.-H. Ho et al, “Smart Simulation Using Collaborative Formal and Simulation
Engines”, Proceedings of ICCAD, pp. 120-126, November 2000
Y. Hoskote, T. Kam, P. Ho and X. Zhao, ``Coverage Estimation for Symbolic Model
Checking'', Proc. of the 36th Design Automation Conference, New Orleans, June 1999.
S. Katz, O. Grumberg and D. Geist, ``Have I written enough properties? - A method of
comparison between specification and implementation'', Technical Report, IBM Haifa
Research Laboratory, Haifa, Israel, 1999.
Model Checking in Practice

S. Berezin, S. Campos and E. M. Clarke, ``Compositional Reasoning in Model
Checking'', Technical Report - CMU-CS-98-106, School of Computer Science, Carnegie
Mellon University, February, 1998.
Papers

K. L. McMillan, "A compositional rule for hardware design refinement", Computer
Aided Verification (CAV97), O. Grumberg (Ed.), Haifa, Israel, pp. 24-35, 1997.

T.A.Henzinger, S. Qadeer, and S.K.Rajamani, "You assume, We guarantee :
Methodology and Case Studies" CAV98: Computer Aided Verification, Lecture Notes in
Computer Science, Springer-Verlag, pp. 440-451, 1998.

G. Mosensoson, “Practical Approaches to SoC Verification”, DATE 2000.

J. L. Nielsen, H. R. Andersen, G. Behrmann, H. Hulgaard, K. Kristoffersen and K. G.
Larsen, “Verification of Large State/Event Systems using Compositionality and
Dependency Analysis”, Proceedings of TACAS 1998, LNCS 1384, April 1998.

D. Geist, G. Biran, T. Arons, M. Slavkin, Y. Nustov, M. Farkas, and K. Holtz, “A
Methodology for the verification of a System on Chip”, Proc. Of DAC 1999, pp. 574-579.

A. Evans, A. Silburt, G. Vrckovnik, T. Brown, M. Dufresne, G. Hall, T. Ho and Y. Liu,
“Functional Verification of Large ASICs”, Proc. Of DAC, 1998.

S. Taylor, M. Quinn, D. Brown, N. Dohm, S. Hildebrandt, J. Higgins and C. Ramey,
“Functional Verification of a Multiple-issue, Out-of-Order, Superscalar Alpha Processor
– the DEC Alpha 21264 Microprocessor”, Proc. Of DAC, 1998.

T. Henzinger, X. Liu, S. Qadeer and S. Rajamani, “Formal Specification and Verification
of a Dataflow Processor Array,”Proceedings of ICCAD 1999

D. Wang, “SAT based Abstraction Refinement for Hardware Verification”, Ph.D. thesis,
ECE Dept., Carnegie Mellon University, May 2003

Shankar G. Govindaraju, David L. Dill, Alan J. Hu, and Mark A. Horowitz. "Approximate
Reachability with BDDs using Overlapping Projections,” in Proc. DAC 1998

Gaurishankar Govindaraju, "Approximate Symbolic Model Checking using
Overlapping Projections" Ph.D. thesis, Stanford University, August 2000.
276
Papers
Simulation Based Verification










I. Ghosh and M. Fujita, ``Automatic test pattern generation for functional registertransferlevel circuits using assignment decision diagrams,'' IEEE. Trans. on ComputerAided Design, Vol. 20, No. 3, pp. 402-415, March 2001.
F. Fallah, S. Devadas, and K. Keutzer, ``OCCOM: Efficient computation of observabilitybased code coverage metrics for functional verification,'' IEEE. Trans. on ComputerAided Design, Vol. 20, No. 8, pp. 1003-1015, Aug. 1998.
F. Fallah, S. Devadas, and K. Keutzer, ``Functional vector generation for HDL models
using linear programming and 3-satisfiability,”{\em IEEE. Trans. on Computer-Aided
Design}, Vol. 20, No. 8, pp. 994-1002, Aug. 1998.
S. Ravi, G. Lakshminarayana, and N.K. Jha, ``TAO: Regular expression based high-level
testability analysis and optimization,'' in Int. Test Conf., pp. 331-340, Oct. 1998.
I. Ghosh and S. Ravi, “On automatic generation of RTL validation test benches using
circuit testing techniques,” in Proc. Great Lakes Symposium on VLSI, April 2003.
L. Zhang, I. Ghosh and M. Hsiao, “Efficient sequential ATPG for functional RTL circuits,”
in Proc. International Test Conference, Oct. 2003.
L. Zhang, I. Ghosh and M. Hsiao, “Automatic design validation framework for HDL
descriptions via RTL ATPG,” in Proc. Asian Test Symposium, Nov. 2003
F. Fallah, I. Ghosh, and M. Fujita, “Event driven observability enhanced coverage analysis
of C programs for functional validation,” in {\em Proc. Asia and South Pacific Design
Automation Conference}, Jan. 2003.
K. Ara and K. Suzuki, “A proposal for transaction level verification with component
wrapper language,” Proc. Design Automation and Test in Europe, March 2003.
A. U. Shankar, "An Introduction to Assertional Reasoning for Concurrent Systems", ACM
Computing Surveys, Sept. 1993, Vol 25, No. 3, pp. 225-262
277
278
Papers

S. Ramesh and P. Bhaduri, “Validation of Pipelined Processor Designs using Esterel
Tools: A Case Study”, Proc. of CAV '99, LNCS Vol. 1633, 1999.

C. Eisner et. al. “The Temporal Logic Sugar” in Proc. Int Conf. on Computer-aided
Verification 2001.
Miscellaneous





J. Jain, W. Adams and M .Fujita, “Sampling Schemes for Computing OBDD Variable
Orderings”, Proceedings of ICCAD 1998, pp. 331-338
J. Jain, R. Mukherjee and M. Fujita, “Advanced Verification Technique Based on
Learning”, Proceedings of DAC 1995, pp. 420-426
C. H. Yang and D. L. Dill, “Validation with Guided Search of the State Space”,
Proceedings of DAC 1998
A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation”, Ph.D.
Thesis, Dept. of Electrical and Computer Engineering, Carnegie Mellon University,
August 1997
C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of
Partially Ordered Trajectories”, Formal Methods in System Design, Vol. 6, No. 2, pp.
147-190, 1995
279
Important web-sites
http://www.comlab.ox.ac.uk/archive/formal-methods.html
http://www.csl.sri.com
http://www-cad.eecs.Berkeley.edu/ vis
http://godel.ece.utexas.edu/texas97-benchmarks/
http://citeseer.nj.nec.com/
http://www.rational.com/uml (Universal Modelling Language HOME-PAGE)
http://www-sop.inria.fr/meije/verification/esterel
http://www.accellera.org
http://www.systemC.org
http://www.specC.org
280
Conference Proceedings

Computer Aided Verification (CAV)

Formal Methods in Computer Aided Design (FMCAD)

International Conference on Computer-Aided Design (ICCAD)

International Conference on Computer Design (ICCD)

Design Automation Conference (DAC)

Asia South Pacific Design Automation Conference (ASPDAC)

International Conference on VLSI Design (VLSI)

Advanced Research Working Conference on Correct Hardware
Design and Verification Methods (CHARME)
281
Journals/Magazines

IEEE Design and Test of Computers

IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems

IEEE Transactions on Computers

IEEE Transactions on VLSI Systems



ACM Transactions on Design Automation of Electronic Systems
Formal Methods in System Design
Formal Aspects of Computing

Religious Language - St Crispin`s School

Procedure for Education Verification

BEE Certificate - Mkhabela Huntley Adekeye

Independent Checking Function Assessment Iain Higgins

BEE Certificate

Board Meeting Agenda - Kokomo-Howard County Public Library

“Ready for the Future Technology today” 2014

I-9 Instructions

Document

English Language Proficiency - OGAPS