ECE 479: Formal Verification
Intro to Formal Verification
Formal verification is used to verify correctness of hardware designs.
Take the example of a 4-bit multiplier with an 8-bit output. There are $2^8$ possible different combinations of inputs. This simple rule is with $n$ inputs, to test fully, you have to test $2^n$ inputs. However, with modern processors being 64-bits, there are $2^128$ inputs to a multiplier. This is too many inputs to be able to test in a reasonable amount of time.
2% of time is design, 98% is testing and finding/fixing bugs.
Formal verification is usually reserved for safety-critical applications such as pacemakers. It is also used where bugs can't be fixed and in production and are expensive to fix.
Some prominent bugs that could have be solved using formal verification include:
- FDIV bug - Intel Pentium processors had a bug in the division table that almost killed them
- Arian 5 Rocket Explosion
In the hardware industry, the cost to fix mistakes is enormous so, we can't afford to make such mistakes.
What is Formal Verification
Let's start with a basic algebraic expression:
$(x+y)^2 = x^2 + y^2 + 2xy$
Formal verification is using mathematical reasoning to prove software/hardware designs, without having to exhaustively test. In this class, we will learn how to prove hardware/software design.
Boolean Satisfiability (SAT)
Allows you to do proofs on boolean expressions.
Basics:
- Boolean variables $x_1, x_2, ... \epsilon {0, 1}$
- Boolean functions $F(x_1, ..., x_n) \epsilon {0, 1}$
Given function F, check if F is satisfiable. In other word, you have to check if there is a valuation (value) for all inputs such that F is true.
Example:
$F = x{1} x{2} x{3} + x{1}' x_{3}$
What are the evaluations that make F true?
$x_1=0, x_2=X, x_3=1$
$x_1=1, x_2=1, x_3=1$
Satifiability just means, can you find at least one set of inputs that makes the function true.
Example:
$G = (x_1 + x_2) (x_1' x_2')$
Which evaluations make G true?
None! This function always evaluates to false.
F is a satisfiable function. G is unsatisfiable.
How can you prove terms with this?
Let's say you have a function f:
$f(x_1, ..., x_n)$
If $f'$ is unsatisfiable, that means $f'$ is always false and therefore, $f$ is always true. So, $f$ is a theorem.