ECE 479: Formal Verification

BDD Properties

1. Satisfiablity: If ROBDD has terminal node $1$, then it is satisfiable.
2. UNSAT: If 0 is the only terminal node
3. Tautology: Function is always true. If 1 is the only terminal node

APPLY Procedure

Allows you to compute the BBD without a truth table.

If you are given two RBBD, you can compute operations between the two BBDs. (e.g. if you have two RBBDs, $R_1$ and $R_2$, you can do $R_1 + R_2 = R_3$ for any operation)

Let's say you have the circuit (x * y) + z'.

Shannon's Expansion: $f = x'f{x \leftarrow 0} + xf{x \leftarrow 1}$

Example

Let's take function f:
$f = abc + a'd$
$f{x \leftarrow 0} = d$
$f{x \leftarrow 1} = bc$

APPLY is based on Shannon's expansion.

Let's say you have $f op g = x'(f{x \leftarrow 0} op g{x \leftarrow 0}) + x(f{x \leftarrow 1} op g{x \leftarrow 1})$

You keep applying this until you get to your terminal nodes.

Recursive Procedure:
$r_f$, $r_g$ are your root nodess of $f$ and $g$.

1. Base Case: If $r_f$ and $r_g$ are terminal nodes, return $r_f op r_g$
2. Recursive Step: $x$ is the splitting variable. $x = min(var(r_f), var(r_g))$

Let's take the two RBBDs:
$r_f$:
$r_g$:
with the ordering $a < b < c < d < x_1 < x_2$

So, based on this ordering, the splitting variable with be $b$. We then use the splitting variable to compute the Shannon's expansion.

$f_{x \leftarrow b} = r_f, x < var(r_f)$
$lo(r_f), x = var(r_f) and b = 0$
$hi(r_f), x = var(r_f) and b = 1$

Example

$r_f =$ $r_g =$

Order: $a < b < c < d$

And we want to compute $f + g$

First, we label the nodes:

$var(A_1) = a$
$var(B_1) = b$
Therefore, the splitting variable is $a$

So we put $a$ as the root node and check if the splitting variable is less than $var(r_f)$

Our new graphs now looks like:

Now, we recursivly apply the algorithm.

The splitting variable is now $b$. We see that for $r_f$, $b$ is equals $var(r_f)$. However, for $r_b$, we see that $var(r_f)$ is lower ($d$) than it, so we just return the root node ($B_2$).

Our graphs now look like:

Now we apply it APPLY to $A_2, B_2$. Our splitting variable is now $d$. Since they are both the splitting variable, you go to the lower children.

Our graphs now look like:

Now that we have reach the terminal nodes, we apply the operation and add it to the graph.

Now we have to go back up and do the rest of the tree.

We go to $A_6$ and see that $B_2$ is less than $A_6$ so we keep $B_2$ and add it to our graphs. The variable will be $c$.

We now keep repeating the process until the tree is complete:

APPLY in Practice

If you have a complex circuit, you can use APPLY recursivly instead of needing any truth tables like so: