Formal Equivalence

Checking
Virendra Singh
Associate Professor
Computer Architecture and Dependable Systems Lab
Dept. of Electrical Engineering
Indian Institute of Technology Bombay, Mumbai
viren@ee.iitb.ac.in

EE 709: Testing & Verification of VLSI Circuits

Lecture – 6 (Jan 17, 2012)
 SoC Verification
• System-on-Chip (SOC) design
• Increase of design complexity
• Move to higher levels of abstraction
Level Number of components

1E0
System level
1E1

Algorithm 1E2

Abstraction

Accuracy
1E3
RTL
1E4

1E5
Gate
1E6
Transistor 1E7

Jan 17, 2012 EE-709@IITB 2

 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 Pipeline IF FSM
IP Netlist
Memory IP
Comp. RAM
State
PC
Interface Interface IR

Bus Control Datapath IF FSM

Memory
Interface
Interface Mem RF
Processors Registers State State
IPs ALUs/FUs
Memories Memory Memories
ALU
Busses Gates
Custom HW

Specification System architecture RTL/IS Implementation

+ constraints + estimates + results

Jan 17, 2012 EE-709@IITB 3

 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
Jan 17, 2012 EE-709@IITB 4
 System-level design & verification
3 minutes
System-level
delay

RTL
3 days
delay

Transistor level 3 weeks

delay

Cost due to the delay/late time-to-market

Bugs fix time
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 5
 Formal verification
• “Prove” the correctness of designs
– Both design and spec must be represented with
mathematical models Spec Design
– Mathematical reasoning
– Equivalent to “all cases” simulations
• Possible mathematical models Front-end
– Boolean function (Propositional logic) tool
• How to represent and manipulate on computers
– First-order logic
• Need to represent “high level” designs Mathematical
– Higher-order logic models
• Theorem proving = Interactive method
• Front-end is also very important
– Often, it determines the total performance of the Verification
tools engines

Jan 17, 2012 EE-709@IITB 6

Backgrounds technology in formal verification
• Methods for reasoning about
mathematical models
Spec Design
– Boolean function (Propositional logic)
• SAT (Satisfiability checker)
Front-end
• BDD (Binary Decision Diagrams) tool

– First-order logic
• Logic of uninterpreted functions Mathematical
with equality models
– Higher-order logic
• Theorem proving = Interactive Verification
method engines

Jan 17, 2012 EE-709@IITB 7

 Formal Equivalence Checking

Jan 17, 2012 EE-709@IITB 8

 Formal Equivalence Checking

Jan 17, 2012 EE-709@IITB 9

 Formal Equivalence Checking
• Equivalence checking can be applied
at or across various levels

Jan 17, 2012 EE-709@IITB 10

 CEC in Practice
Key observation: The circuit being verified usually have
a number of internal equivalent functions

Jan 17, 2012 EE-709@IITB 11

 Formal Equivalence Checking
Canonical Forms
a
f = ab + c
b
a b c f
c 0 0 0 1
0 0 1 0
0 1 0 1
a 0 1 1 0
F’ = (a+ c)(b+c)
1 0 0 1
1 0 1 1
b
1 1 0 1
c 1 1 1 1

Jan 17, 2012 EE-709@IITB 12

 Formal Equivalence Checking

Complexity
 Efficiency of the conversion to canonical form
Memory requirement
Efficiency of the comparison of two
representation of the canonical form
Efficiency to generate the counter example in
case of a miscompare

Jan 17, 2012 EE-709@IITB 13

 Formal Equivalence Checking
• Satisfiability Formulation A 0
1 T3
– Search for input assignment B 1 1 O2
1
giving different outputs C Diff
0 T1
• Branch & Bound A 0 0
1 1
– Assign input(s) C
1 O1
– Propagate forced values B 1
T2
– Backtrack when cannot succeed

• Challenge
– Must prove all assignments fail
• Co-NP complete problem
– Typically explore significant
fraction of inputs
– Exponential time complexity

Jan 17, 2012 EE-709@IITB 14

 Formal Equivalence Checking

 Canonical form representation is only

suitable
 DNF and CNF are not suitable
 BDD is most popular canonical form
 graphical representation of boolean
function

Jan 17, 2012 EE-709@IITB 15

 Formal Equivalence Checking
 BDD is canonical form of representation
 Shanon’s expansion theorem
 f(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) f(x1, x2, … ,xi=1, ……xn)

Jan 17, 2012 EE-709@IITB 16

 Binary Decision Diagram
• Generate Complete Representation of Circuit Function
– Compact, canonical form
a

A T1 b
O1
C c

B T2 0 1

a
A T3
B O2 b
C c

0 1

 Functions equal if and only if representations identical

 Never enumerate explicit function values
 Exploit structure & regularity of circuit functions

Jan 17, 2012 EE-709@IITB 17

 Decision Structures

Truth Table Decision Tree

x 1 x2 x3 f
x1
0 0 0 0
0 0 1 0
0 1 0 0 x2 x2
0 1 1 1
1 0 0 0
1 0 1 1 x3 x3 x3 x3
1 1 0 0
1 1 1 1
0 0 0 1 0 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.
Jan 17, 2012 EE-709@IITB 18
 Variable Ordering
Assign arbitrary total ordering to variables
 e.g., x1 < x2 < x3
Variables must appear in ascending order along all
paths
OK Not OK
x1 x1 x3 x1

x2 x2

x3 x3 x1 x1

Properties
 No conflicting variable assignments along path
 Simplifies manipulation
Jan 17, 2012 EE-709@IITB 19
 Reduction Rule #1
Merge equivalent leaves

a a a

x1 x1

x2 x2 x2 x2

x3 x3 x3 x3 x3 x3 x3 x3

0 0 0 1 0 1 0 1 0 1

Jan 17, 2012 EE-709@IITB 20

 Reduction Rule #2

Merge isomorphic nodes

x x x x x x

y z y z y z

x1 x1

x2 x2 x2 x2

x3 x3 x3 x3 x3 x3

0 1 0 1

Jan 17, 2012 EE-709@IITB 21

 Reduction Rule #3
Eliminate Redundant Tests

y y

x1 x1

x2 x2 x2

x3 x3 x3

0 1 0 1

Jan 17, 2012 EE-709@IITB 22

 Example OBDD

Initial Graph Reduced Graph

x1 x1 (x1+x2)· x3

x2 x2 x2

x3 x3 x3 x3 x3

0 0 0 1 0 1 0 1 0 1

• Canonical representation of Boolean function

 For given variable ordering
 Two functions equivalent if and only if graphs isomorphic
o Can be tested in linear time
 Desirable property: simplest form is canonical.
Jan 17, 2012 EE-709@IITB 23
 Example Functions
Constants Variable
0 Unique unsatisfiable function x
Treat variable
1 Unique tautology as function
0 1

Typical Function Odd Parity

x1  (x1  x2 )  x4 x1

 No vertex labeled x3
x2 x2 x2 Linear
 independent of x3 representation
 Many subgraphs shared x3 x3

x4 x4 x4

0 1 0 1

Jan 17, 2012 EE-709@IITB 24

 Representing Circuit Functions
• Functions
S3 Cout
– All outputs of 4-bit adder
– Functions of data inputs a3 a3

S2 b3 b3 b3 b3

A a2 a2 a2
Cout
A
D S1 b2 b2 b2 b2 b2 b2
S
D
B a1 a1 a1

S0 b1 b1 b1 b1 b1 b1
• Shared Representation
– Graph with multiple roots a0 a0 a0
– 31 nodes for 4-bit adder b0 b0
– 571 nodes for 64-bit adder
0 1
Linear growth
Jan 17, 2012 EE-709@IITB 25
 Effect of Variable Ordering
(a  b )  (a  b )  (a  b )
1 1 2 2 3 3
Good Ordering Bad Ordering
a1 a1

b1 a2 a2

a2 a3 a3 a3 a3

b2 b1 b1 b1 b1

a3 b2 b2

b3 b3

0 1 0 1
Linear Growth Exponential Growth
Jan 17, 2012 EE-709@IITB 26
 Selecting Good Variable Ordering
• Intractable Problem
 Even when problem represented as OBDD
i.e., to find optimum improvement to current ordering
• Application-Based Heuristics
 Exploit characteristics of application
 e.g., Ordering for functions of combinational
circuit
Traverse circuit graph depth-first from outputs to inputs
Assign variables to primary inputs in order encountered

Jan 17, 2012 EE-709@IITB 27

 Selecting Good Variable Ordering
Static Ordering
 Fan In Heuristic
 Weight Heuristic
Dynamic Ordering
 Variable Swap
 Window Permutation
 Sifting

Jan 17, 2012 EE-709@IITB 28

 Swapping Adjacent Variables
 Localized Effect
 Add / delete / alter only nodes labeled by swapping variables
 Do not change any incoming pointers

g h i j e f g h
b1 b1 b1 b1 b2 b2 b2 b2
f i j
e
b2 b2 b1 b1

Jan 17, 2012 EE-709@IITB 29

 Dynamic Variable Reordering
Richard Rudell, Synopsys
Periodically Attempt to Improve Ordering for
All BDDs
Part of garbage collection
Move each variable through ordering to find its
best location
Has Proved Very Successful
Time consuming but effective
Especially for sequential circuit analysis

Jan 17, 2012 EE-709@IITB 30

 Dynamic Reordering By Sifting
 Choose candidate variable Best
 Try all positions in variable ordering Choices
Repeatedly swap with adjacent variable
 Move to best position found
a1 a1 a1 a1 b1

a2 a2 a2 a2 a2 a2 b1 a1

a3 a3 a3 a3 a3 a3 a3 a3 b1 b1 a2 a2

b2 b2 b2 b2 b2 b2 b2 b2 ••• a3 a3 a3 a3 a3 a3

b1 b1 b3 b3 b2 b2 b2 b2 b2 b2

b3 b1 b3 b3 b3

0 1 0 1 0 1 0 1 0 1

Jan 17, 2012 EE-709@IITB 31

 ROBDD sizes & variable ordering
• Bad News 
– Finding optimal variable ordering NP-Hard
– Some functions have exponential BDD size for all orders
e.g. multiplier
• Good News 
– 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)

Jan 17, 2012 EE-709@IITB 32

 Thank you

Jan 17, 2012 EE-709@IITB 33