Verification of digital circuit verification
Chih-Sheng Chang, a summer intern of mine (who’s entering his third year at NTU’s Department of Electrical Engineering), mentioned to me a project he worked on, which used a SAT solver to verify the behaviour of a digital circuit design (built out of logic gates) against a reference one, and asked whether we can model the verification method in Agda and prove some of its properties. Yes of course!
Starting with a reference circuit $R$, we may want to construct a more optimised implementation circuit $I$ and verify that its behaviour agrees with $R$. The way Chih-Sheng did the verification was to construct a larger ‘tester’ circuit that passes the input bits to both $R$ and $I$ and compares their corresponding output bits. This is illustrated in the following diagram, where the comparisons are performed using XNOR gates (which output $1$ if and only if the two input bits are the same).
Now $R$ and $I$ exhibit the same behaviour if and only if the output bits of the tester circuit are always $1$ for all inputs. The latter condition can be verified by employing the standard Tseitin transformation to turn the tester circuit into a boolean formula $F(\vec x, \vec y, \vec z)$ (in conjunctive normal form) where $\vec x$ are the variables representing the inputs, $\vec y$ the outputs, and $\vec z$ some intermediate values, and then checking that the formula $F(\vec x, \vec y, \vec z) \wedge \bigvee \neg \vec y$ — which says that the tester circuit maps input $\vec x$ to output $\vec y$ and that some of the output bits are false, indicating disagreement between $R$ and $I$ — is unsatisfiable by SAT solving (which means that there is no disagreement).
There is a twist, however. Conceptually, the circuits considered by Chih-Sheng are not exactly boolean: in addition to $0$ and $1$, a wire can also carry the value $\mathsf X$ which represents the situation where the exact value is unknown. Consequently, the logic becomes three-valued, and the definitions of all the logic gates have to be extended to the three-valued setting. For example, the truth table of the three-valued AND gate is
$$ \begin{array}{c|ccc} & 0 & \mathsf X & 1 \\ \hline 0 & 0 & 0 & 0 \\ \mathsf X & 0 & \mathsf X & \mathsf X \\ 1 & 0 & \mathsf X & 1 \end{array} $$
which makes sense if we interpret $\mathsf X$ as ‘a value that may be 0 or 1’ (but we don’t know which). What’s particularly interesting is that the gate used for comparing the output bits is extended asymmetrically, since in the three-valued setting we do not require that $R$ and $I$ behave exactly the same, but only that $I$ ‘refines’ $R$ — that is, given an input, if $R$ outputs something definite (i.e., $0$ or $1$), then $I$ ought to output the same thing, but if $R$ outputs $\mathsf X$, then $I$ can output anything. Formally, the three-valued comparison gate is defined by
$$ \begin{array}{c|ccc} & 0 & \mathsf X & 1 \\ \hline 0 & 0 & 1 & 1 \\ \mathsf X & 0 & 0 & 0 \\ 1 & 1 & 1 & 0 \end{array} $$
where the argument on the left is the reference bit and the argument on the top is the implementation bit. Now, to perform the verification, the three-valued tester circuit is first ‘desugared’ to a boolean circuit by replacing (i) each three-valued wire with two boolean wires, where one of the wires indicates whether the value is known and, if it is known, the other carries the actual value, and (ii) each three-valued logic gate with its implementation in terms of boolean logic gates. The resulting boolean circuit can then be verified as before.
An observation made during a meeting with Chih-Sheng and Liang-Ting was that there may be an alternative way to arrive at a boolean formula from a three-valued circuit. The above two-step process first transforms ‘three-valuedness’ into ‘booleanness’, and then transforms a circuit to a formula (for SAT solving). Hypothetically, there should be an alternative process where we first transform a (three-valued) circuit to a formula, which is then transformed to a boolean one. The two processes could then be shown to be equivalent in some sense (e.g., equi-satisfiability). Hmm, something verifiable in Agda! Alas, the workload seems to be too heavy for Chih-Sheng’s remaining time here. We have to aim for something more straightforward (but still interesting enough).
What we set out to do is verify that the desugaring of three-valued circuits to boolean ones is semantics-preserving. In fact it is easy to generalise the desugaring a bit and make it more useful: instead of just dealing with three-valued circuits, we can deal with arbitrarily typed circuits as long as the types have a finite representation (so that we can replace a wire of a given type with a fixed number of boolean wires). Since circuits are essentially programs made up of let-expressions, what we will achieve is a semantics-preserving translation of simple, finitely typed programs to bit-manipulating programs, the latter of which are amenable to SAT-based verification techniques. This also readily allows the optimisation of the number of boolean wires used in the resulting circuit, since we can determine more precisely how many boolean wires should be used for each wire in the original circuit based on the type of the wire. For example, the result of a three-valued comparison gate is necessarily boolean, so we can make the result type $\mathsf{Bool}$, and the translation will use just one wire to represent the output of the gate.
More technically: The types of circuit programs take the form $\mathsf{Circuit}\ \Gamma\ \Delta$ where $\Gamma$ is an association list of input variables and their types, and $\Delta$ is a list of output types. The circuit language has only two constructs, a $\mathsf{return}$ expression that selects some of the input variables $\vec x$ as outputs,
$$ \frac{\Gamma \vdash \vec x : \Delta}{\mathsf{return}\ \vec x : \mathsf{Circuit}\ \Gamma\ \Delta} $$
and a specialised $\mathsf{let}$-expression that applies a $\mathit{gate}$ to some of the input variables $\vec x$, binds the output of the gate to a new variable $y$, and continues with a circuit program $C$ that can access the new variable $y$ in addition to those originally available:
$$ \frac{\mathit{gate} : \Sigma \Rightarrow \tau \qquad \Gamma \vdash \vec x : \Sigma \qquad C : \mathsf{Circuit}\ (\Gamma, y : \tau)\ \Delta}{\mathsf{let}\ y = \mathit{gate}\ \vec x\ \mathsf{in}\ C : \mathsf{Circuit}\ \Gamma\ \Delta} $$
The semantics of a circuit $C : \mathsf{Circuit}\ \Gamma\ \Delta$ is a function $\sem{C} : \sem{\Gamma} \to \sem{\Delta}$ that maps a product of values whose types are exactly those in $\Gamma$ to a product of values similarly typed by $\Delta$. To compile a circuit to a boolean one, we use a function
$$ \mathsf{compile} : \mathsf{Circuit}\ \Gamma\ \Delta \to \mathsf{Circuit}\ (\mathsf{encodeTypes}\ \Gamma)\ (\mathsf{encodeTypes}\ \Delta) $$
where $\mathsf{encodeTypes}$ (metaphorically speaking) turns a list of typed wires into a list of boolean wires that can represent the same range of values. The key property of $\mathsf{compile}$ is the equation
\begin{equation} \sem{C} \circ \mathsf{decode} = \mathsf{decode} \circ \sem{\mathsf{compile}\ C} \label{eq:compile-correctness} \end{equation}
where $\mathsf{decode} : \sem{\mathsf{encodeTypes}\ \Gamma} \to \sem{\Gamma}$ reconstructs a list of typed values from their binary representations; ideally it should be a surjection, as we will see below. Equation \ref{eq:compile-correctness} is all we need for reducing equations about typed circuits to equations about boolean circuits (the latter of which are then verified by SAT solving): for example, if we want to prove that the output of a circuit $C : \mathsf{Circuit}\ \Gamma\ \mathsf{Bool}$ is constantly $1$, we can compile it to a boolean circuit $\mathsf{compile}\ C : \mathsf{Circuit}\ (\mathsf{encodeTypes}\ \Gamma)\ \mathsf{Bool}$ and use a SAT solver to prove
$$ \forall y : \sem{\mathsf{encodeTypes}\ \Gamma}.\ \sem{\mathsf{compile}\ C}\ y = 1 $$
and this will lead to what we want for $C$: Applying $\mathsf{decode}$ to both sides of the equation (and assuming $\mathsf{decode}$ behaves as the identity function for $\mathsf{Bool}$), we get
$$ \forall y : \sem{\mathsf{encodeTypes}\ \Gamma}.\ \mathsf{decode}\ (\sem{\mathsf{compile}\ C}\ y) = 1 $$
Equation \ref{eq:compile-correctness} allows us to rewrite the left-hand side and get
$$ \forall y : \sem{\mathsf{encodeTypes}\ \Gamma}.\ \sem{C}\ (\mathsf{decode}\ y) = 1 $$
If $\mathsf{decode}$ is surjective, $\mathsf{decode}\ y$ above will range over the entire domain of $\sem{C}$, and we will arrive at
$$ \forall x : \sem{\Gamma}.\ \sem{C}\ x = 1 $$
as required. And Equation \ref{eq:compile-correctness} itself shouldn’t be too hard to verify: we should be able to prove a similar equation for each gate we want to use, and then all it takes should be just an induction on the program structure.
This circuit language is fairly simplistic: there are no abstraction features (we can’t even express the circuit diagram at the beginning of this post), recursive/infinite types, or loops (the $\mathsf{let}$-expressions are non-recursive). As a result, we’re only considering finitely typed non-recursive functions whose structures are as simple as an intermediate language, which PLT people will easily dismiss. Still, I’d be interested to know how well the verification method scales as the circuit complexity increases, just to get a feel of how easy or hard it is to harness the power of SAT solving.
