Use of BDDs for Verification

Use of BDDs for Verification

0

X1

X2

X2

X3

X3

1

0

1

1

m Condition on edges forces order on variables.

m Order must be consistent with all edges.

m For each edge, parent before child in the order.

Ô X1 X2 X3

Previous slide

Next slide

Back to the first slide

View Graphic Version