ECE 479: Formal Verification
SATEquivalence Checking
If you want to take the equivalence of two circuits, first wire the inputs together and then AND together the XNORs of each output. So for each input, F should always be 1.
Multiplier Problem
How to verify a new 64-bit multiplier by comparing to an existing multiplier?
We first create a circuit around the multipliers:
This as an equation will look like:
$f(x_1,...,x_64,y_1,...,y_64)$
Is $f'$ UNSAT?
If it is SAT, then that means there is some combination inputs for which the outputs don't agree.
Example
SAT $f=xy+x'z$
x | y | z | xy | x'z | f |
---|---|---|---|---|---|
0 | 0 | 0 | 0 | 0 | 0 |
0 | 0 | 1 | 0 | 1 | 1 |
0 | 1 | 0 | 0 | 0 | 0 |
0 | 1 | 1 | 0 | 1 | 1 |
1 | 0 | 0 | 0 | 0 | 0 |
1 | 0 | 1 | 0 | 0 | 0 |
1 | 1 | 0 | 1 | 0 | 1 |
1 | 1 | 1 | 1 | 0 | 1 |
Is this function satisfiable? YES
Because there are inputs that result in a true output.
How to check if F is SAT
- Draw truth table - If all outputs = 0, then UNSAT, otherwise SAT
- DPLL
DPLL
What modern SAT solvers are based on. It takes a boolean function as the input and it will tell you if the function is satisfiable. To do this, it has to be in Products of Sums (POS) format and Conjunctive Normal Form (CNF).
Example
Will take multiple classes to complete.
Clauses | POS |
---|---|
$C_1$ | $(a'+b+c)$ |
$C_2$ | $(a+c+d)$ |
$C_3$ | $(a+c+d')$ |
$C_4$ | $(a+c'+d)$ |
$C_5$ | $(a+c'+d')$ |
$C_6$ | $(b'+c'+d)$ |
$C_y$ | $(a'+b+c)$ |
$C_y$ | $(a'+b'+c)$ |
First, we make a decision on one of the varibles (in this case, a) and assign it the value of 0. We then see if that makes any of the clauses true.
In the current case, we see that it makes $C_1$, $C_7$, and $C_8$.
a=0
$C_1:(a'+b+c)=(0'+b+c)=(1+b+c)=1$
So, now we remember which clauses get satisfied for each decision. The goal is to keep making decisions and then it sees how many clauses are satisfied. If all clauses are satisfied, then the whole function is satisfied.
So now, lets set $b$ to $0$.
a=0,b=0 : $C_1$,$C_7$,$C_8$
This adds $C_6$.
a=0,b=0,c=0 : $C_1$,$C_6$,$C_7$,$C_8$
This adds $C_4$ and $C_5$.
a=0,b=0,c=0 : $C_1$,$C_4$,$C_5$,$C_6$,$C_7$,$C_8$
To draw this process, follow a tree-like structure
We will continue next class.