Introduction to Formal Verification and Logic Synthesis

Introduction to Formal Verification and Logic Synthesis

Yukio Miyasaka

Contents

Formal Verification ? Equivalence Checking

? Binary Decision Diagram ? Boolean Satisfiability Problem

Logic Synthesis ? Two-Level Logic Synthesis ? Two-Level Logic to Multi-Level Logic ? Multi-Level Logic Optimization

Formal Verification

? Prove that a given logic circuit meets some given properties ? Often compared to random simulation, here are some tradeoffs:

Coverage Time

Formal Verification 100%

~O(exp(circuit size))

Random Simulation #test patterns / #all possible patterns

O(#test patterns * circuit size)

Note: coverage has a different meaning for bounded model checking

Equivalence Checking

? Given two implementations, prove they are functionally equivalent

? For simplicity, assume the implementations are combinational logic circuits ? Optimized implementation v.s. Golden model (Spec)

? Exhaustive simulation is enough to prove this property ? However, it takes an exponential amount of time

? N inputs -> 2^N patterns to simulate ? O(exp(#inputs))

? Can we do it better?

Binary Decision Diagram (BDD)

? Binary tree ? Redundant nodes (equivalent cofactors) are removed ? Each node has a unique function

Randal E. Bryant, "Symbolic Boolean manipulation with ordered binary-decision diagrams," in ACM Computing Surveys, vol. 24, no. 3, pp. 293?318, 1992.

BDD Operations

? We can construct a BDD for the result of operation by a recursive procedure ? e.g. BDD z = AND(BDD x, BDD y);

? Runtime is bounded by O(#BDD nodes) while #BDD nodes is usually smaller than exp(#inputs)

x

y

z

Symbolic Simulation

n13

x0

1c4

x2

1c3

x0

0

1

x2

x1

n15

x1

1cb

x2

1ca

x3

1c5

0

1

x2 x3

n12

x2

1c4

x3

1c3

0

1

x4

n14

x2

1c8

x3

1c7

x4

1c6

0

1

Output BDDs to be compared with the golden model

n16

x0

1d3

x1

1d2

1cc

x2

1d1

1c5

y0 x3

1d0

0

1

y1 x1 x2 x3 x4

n17

1da

1d7

1d9

1c6

1d8

1cd

1

0

Boolean Satisfiability Problem

? Problem definition . = 1.

? One of the most famous NP-complete problems

? is usually given as CNF (Conjunctive Normal Form) a.k.a. POS

? Variable ? Literal ? Clause ? CNF

1, 2, ... 1, 1 , 2, 2 , ... 1 + 2 + 3, ... ...

? Many heuristics have been proposed

? Can be solved much faster than the other NP-complete problems

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download