Use of BDDs for Verification

Use of BDDs for Verification

0

X1

X2

X2

X3

X3

1

0

1

1

V1

V2

V3

m V1 is a redundant vertex

m V2, V3 represent the same function

m A BDD is a reduced binary decision graph

Ô Reduction is O(N*log(N)) for N verticies

Previous slide

Next slide

Back to the first slide

View Graphic Version