Design Verification
An Introduction
Virendra Singh
Associate Professor
Computer Architecture and Dependable Systems Lab
Department of Electrical Engineering
Indian Institute of Technology Bombay
http://www.ee.iitb.ac.in/~viren/
E-mail: viren@ee.iitb.ac.in
EE-709: Testing & Verication of VLSI Circuits
Lecture 1 (12 Jan 2015)
CADSL!
VLSI Realization Process
Customers need
Determine requirements
Write specifications
Design synthesis and Verification
Test development
Fabrication
Manufacturing test
Chips to customer
12 Jan 2015
EE-709@IITB
CADSL!
Design Synthesis Flow
RTL Design
Synthesis &
optimization
Routing
ECO
DFT insertion
IO Insertion
Placement
Clock tree synthesis
12 Jan 2015
EE-709@IITB
CADSL!
Timeline of Design Cycle
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
0%
13%
10% 20% 30% 40% 50% 60%
Bo#lenecks
in
Design
Cycles:
Survey
of
545
engineers
by
EETIMES
2000
12 Jan 2015
CADSL!
Definitions
v Design
synthesis:
Given
an
I/O
funcCon,
develop
a
procedure
to
manufacture
a
device
using
known
materials
and
processes.
v Verica1on:
PredicCve
analysis
to
ensure
that
the
synthesized
design,
when
manufactured,
will
perform
the
given
I/O
funcCon.
v Test:
A
manufacturing
step
that
ensures
that
the
physical
device,
manufactured
from
the
synthesized
design,
has
no
manufacturing
defect.
12 Jan 2015
EE-709@IITB
CADSL!
Verification of DVD Player
DVD
Player
6
inputs
Stop
Nothing
is
pressed
Play,
Pause,
Stop
Play
Rew
FF,
Rew
Internal
5
States
Pause
FF
Stopped,
Paused
Play
at
normal
speed
Forward
at
2X
speed
Rewind
at
2X
speed
12 Jan 2015
EE-709@IITB
CADSL!
Verification of DVD Player
Assume
1024
x
786
pixels
True
colour
(32
bits)
Number
of
discrete
states
=
(232)(1024x786)
CombinaCon
of
current
states
to
next
states
[(232)(1024x786)]2
Pixels
are
independent
Bounded
number
of
total
states:
No.
of
pixels
x
number
of
possible
colours
x
number
of
internal
state
machines
1024x786x232x5
=
16,888,498,602,639,360
All
transiCons
from
current
state
to
next
states
are
considered
12 Jan 2015
EE-709@IITB
CADSL!
Verification of DVD Player
Number
of
possible
next
states:
No.
of
pixels
x
number
of
possible
colours
x
number
of
possible
inputs
1024x786x232x6
=
20,266,198,323,167,232
Possible
current
state
to
possible
next
states
are
to
be
veried
16,888,498,602,639,360
x
20,266,198,323,167,232
=
3.4
x
1032
Assume
a
simulaCon
engine
can
verify
1,000,000
transiCons
per
second
It
needs
10,853,172,947,159,498,300
Years
to
verify
12 Jan 2015
EE-709@IITB
CADSL!
Design Verification
SpecicaCon
AutomaCc
ImplementaCon
(Synthesis)
SimulaCon
with
Checkers/
drivers
SimulaCon
Based
VericaCon
Formal
SpecicaCon
Property
checking
Equivalence
Checking
Formal
VericaCon
Correct-by
ConstrucCon
ImplementaCon
12 Jan 2015
EE-709@IITB
CADSL!
Importance of Formal Verification
SimulaCon
vCan
be
applied
in
any
design
level
vBut
quality
of
vericaCon
fully
depends
on
SimulaCon
Pa#erns
Corner
cases
may
be
missed
Random
is
just
random
and
does
not
cover
corner
cases
EmulaCon
vImplement
on
FPGA
or
other
programmable
device
need
lot
of
preparaCon
vSCll
vericaCon
quality
fully
depends
on
SimulaCon
Pa#erns
corner
cases
problem
remains
Famous
bug:
PenCum
FloaCng
point
bug
-
$500
M
4,195,385/3,145,727
= 1.333820449136241001
= 1.333739068902037589
12 Jan 2015
EE-709@IITB
10
CADSL!
Simulation-Based Verification
Bug
Bug
Initial
State
12 Jan 2015
Bug
Bug
Bug
Bug
EE-709@IITB
11
CADSL!
Simulation Vs Formal Verification
Simulation/emulation
Formal Verification
o Cannot cover all cases
o Corner cases may be
missed
Equivalent to all
case simulation
o Essential method and
good for initially
debugging
No corner case w.r.t
given property
12 Jan 2015
EE-709@IITB
12
CADSL!
Simulation vs Formal Verification
Program testing can be used to show the
presence of the bugs, but never to show the
absence!
(E.W. Dijkstra)
12 Jan 2015
EE-709@IITB
13
CADSL!
Simulation Vs Formal Verification
Example:
Exclusive-OR circuit
z = (~x & y) + (x & ~y)
12 Jan 2015
EE-709@IITB
14
CADSL!
Simulation Vs Formal Verification
Transform the formulae for circuit to the one
for specification by mathematical reasoning
z = ~b + ~c
b = ~x + ~a
c = ~a + ~y
a = ~x + ~y
z = ~b + ~c
= ~(~x + ~a) + ~(~x + ~y)
=a&x+a&y
= (~x + ~y) & x + (~x + ~y )& y
= x & ~y + ~x & y
All transformation are based on axioms and theorems
Mathematical proof of correctness of design
12 Jan 2015
EE-709@IITB
15
CADSL!
Formal Verification
Techniques
v Deductive Verification (Theorem proving)
Uses axioms, rules to prove system correctness
Difficult and time consuming
v Model Checking
Automatic technique to prove correctness of concurrent
systems
Symbolic algorithms (using BDD)
v Equivalence Checking
Check if two circuits are equivalent
12 Jan 2015
EE-709@IITB
16
CADSL!
SoC Verification
System-on-Chip
(SOC)
design
Increase
of
design
complexity
Move
to
higher
levels
of
abstracCon
Algorithm
1E0
1E1
1E2
1E3
RTL
Gate
1E4
Accuracy
System level
Number of components
Abstraction
Level
1E5
1E6
Transistor
12 Jan 2015
1E7
EE-709@IITB
17
CADSL!
System-level design & verification
System-level
3 minutes
delay
3 days
delay
RTL
3 weeks
delay
Transistor level
Bugs fix time
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
12 Jan 2015
EE-709@IITB
18
CADSL!
Formal verification
Prove
the
correctness
of
designs
Both
design
and
spec
must
be
represented
with
mathemaCcal
models
MathemaCcal
reasoning
Equivalent
to
all
cases
simulaCons
Spec
Possible
mathemaCcal
models
Front-end
tool
Boolean
funcCon
(ProposiConal
logic)
How
to
represent
and
manipulate
on
computers
First-order
logic
Need
to
represent
high
level
designs
Higher-order
logic
Theorem
proving
=
InteracCve
method
Mathematical
models
Front-end
is
also
very
important
Ohen,
it
determines
the
total
performance
of
the
tools
12 Jan 2015
EE-709@IITB
Design
19
Verification
engines
CADSL!
Backgrounds Technology in Formal Verification
Methods
for
reasoning
about
mathemaCcal
models
Boolean
funcCon
(ProposiConal
logic)
SAT
(SaCsability
checker)
BDD
(Binary
Decision
Diagrams)
First-order
logic
Logic
of
uninterpreted
funcCons
with
equality
Higher-order
logic
Theorem
proving
=
InteracCve
method
12 Jan 2015
EE-709@IITB
20
Spec
Design
Front-end
tool
Mathematical
models
Verification
engines
CADSL!
Formal Equivalence Checking
12 Jan 2015
EE-709@IITB
21
CADSL!
Formal Equivalence Checking
12 Jan 2015
EE-709@IITB
22
CADSL!
Formal Equivalence Checking
Equivalence
checking can be applied
at or across various levels
12 Jan 2015
EE-709@IITB
23
CADSL!
CEC in Practice
Key
observaCon:
The
circuit
being
veried
usually
have
a
number
of
internal
equivalent
funcCons
12 Jan 2015
EE-709@IITB
24
CADSL!
Formal Equivalence Checking
Canonical Forms
a
f = ab + c
b
c
F = (a+ c)(b+c)
b
c
12 Jan 2015
EE-709@IITB
25
CADSL!
Formal Equivalence Checking
Complexity
Eciency
of
the
conversion
to
canonical
form
Memory
requirement
Eciency
of
the
comparison
of
two
representaCon
of
the
canonical
form
Eciency
to
generate
the
counter
example
in
case
of
a
miscompare
12 Jan 2015
EE-709@IITB
26
CADSL!
Formal Equivalence Checking
ATPG
FormulaCon
Search
for
input
assignment
giving
dierent
outputs
A
B
C
A
C
B
0
1
1
0
1 T3
1
0
Diff
T1
1
1
O2
O1
T2
Challenge
Must
prove
all
assignments
fail
NP
complete
problem
Typically
explore
signicant
fracCon
of
inputs
ExponenCal
Cme
complexity
12 Jan 2015
EE-709@IITB
27
CADSL!
Formal Equivalence Checking
vCanonical
form
representaCon
is
only
suitable
vDNF
and
CNF
are
not
suitable
vBDD
is
most
popular
canonical
form
Graphical
representaCon
of
boolean
funcCon
12 Jan 2015
EE-709@IITB
28
CADSL!
Formal Equivalence Checking
vBDD
is
canonical
form
of
representaCon
vShanons
expansion
theorem
vf(x1,
x2,
.xi,
xn)
=
xi.f(x1,
x2,
,xi=1,
xn)
+
xi.
f(x1,
x2,
,xi=0,
xn)
xi
f(x1, x2, ,xi=1, xn)
12 Jan 2015
f(x1, x2, ,xi=1, xn)
EE-709@IITB
29
CADSL!
Binary Decision Diagram
Generate
Complete
RepresentaCon
of
Circuit
FuncCon
Compact,
canonical
form
a
T1
O1
C
B
T2
A
B
C
T3
c
0
O2
b
c
0
FuncCons
equal
if
and
only
if
representaCons
idenCcal
Never
enumerate
explicit
funcCon
values
Exploit
structure
&
regularity
of
circuit
funcCons
12 Jan 2015
EE-709@IITB
30
CADSL!
Thank You
12 Jan 2015
EE-709@IITB
31
CADSL!
