ECE 479: Formal Verification
BDDImplies 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:
This is the BDD.
Ordered BDD (OBBD)
- Imposes a total ordering over the variables. (e.g. $x_1 < x_2 < x_3$, $x_2 < x_3 < x_1$)
- For any vertex $u$ and non-terminal child $v$, $var(u) < var(v)$
For example, given the following 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)
- Remove duplicate terminal nodes
- 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:
So we see that 5, 6, and 7 are duplicates. - 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
- Satisfiablity: If ROBDD has terminal node $1$, then it is satisfiable.