ECE 479: Formal Verification

BDD

Implies Operator

$a \rightarrow b \equiv a' + b$

If you write the truth table, you will see $a \rightarrow b$ is true for all inputs except when $a = 1$ and $b = 1$.

Binary Decision Diagrams (BDD)

Another widely used algorithm.

$x_1$ $x_2$ $x_3$ $f$
0 0 0 0
0 0 1 0
0 1 0 0
0 1 1 1
1 0 0 0
1 0 1 1
1 1 0 0
1 1 1 1

You can then represent the truth-table graphically. This truth table would look like so:
BDD

This is the BDD.

Ordered BDD (OBBD)

For example, given the following diagram:
Example Diagram

$b$ is the lower child of $a$ ($lo(a)$) $c$ is the higher child of $a$ ($hi(a)$) $x_1, x_2, ...,$ is the non-terminal vertices $0, 1$ is the terminal vertices

Reduced OBBD (ROBBD)

  1. Remove duplicate terminal nodes
    First Step
  2. Remove duplicate non-terminal vertices, if
    a. $var(u) = var(v)$
    b. $lo(u) = lo(v)$
    c. $hi(u) = hi(v)$
    First, name the vertices:
    Named Vertices
    So we see that 5, 6, and 7 are duplicates. Deduplicated Graph
  3. Remove redundant vertices
    Vertex $v$ is redundant if $lo(v) = hi(v)$
    So now we look at the graph and see that 4 and 3 are redundant.

Doing this finally gives us the ROBDD:

Now, to check if this is correct, you can trace all the paths and match with the truth table.

BDD Properties

  1. Satisfiablity: If ROBDD has terminal node $1$, then it is satisfiable.