ECE 479: Formal Verification

SAT

Equivalence 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:
Circuit Design

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

  1. Draw truth table - If all outputs = 0, then UNSAT, otherwise SAT
  2. 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$

Diagram

To draw this process, follow a tree-like structure

We will continue next class.