Mike Gordon and hardware verification
[
]
In the late 1960s, important papers by Robert W. Floyd and Tony Hoare seemed to herald the advent of fully verified software. However progress soon slowed. It became clear that once you moved beyond a simple flowchart program and had to deal with the horrors of procedures, variable scope, and aliasing, things were not so simple. I remember clearly, when I was a student at Stanford, I saw a PhD dissertation boldly titled hardware verificationAnd wondering how the writer (Todd Wagner) must have been out of his mind to tackle something so difficult. I had little doubt that I would soon find a friend and colleague, Mike Gordon, who would make hardware verification a reality, and even make it easy.
modeling hardware
In the early 1980s, when I had joined Mike Gordon’s group at Cambridge, he came to my office and left a preprint titled “A Very Simple Model of CMOS”. (Although I have been unable to find any publication with a similar title.) Shall we work together on this?, he asked. In an unfortunate decision, I said I would prefer to go my own way (which at the time meant automation of type theory), and it is interesting to speculate what might have happened if I had said yes. We never published a single joint paper.
Mike’s fundamental discovery, on which he worked systematically for a decade, was that hardware circuits could be easily modeled using higher order logic. And their approach worked exactly the same whether the components were being combined for individual transistors or were made from thousands of transistors.
His thought was simply this:
- Each device is modeled by a Relationship on its ports, describing what combinations of port values were possible
- No difference between input and output
- port values can be Anything:bits, words, vectors, functions (for time-sequenced signals)
- All in a standard formality, higher-order logic
Here is a device with four ports. We can imagine that $a$ and $b$ are inputs and $c$ and $d$ are outputs, but this is not the model.
The simplest devices include power and ground (represented by T and F), and transistors, such as the following n-channel:
Here we see why the relational model is ideal. The formula for this transistor is $g\to d=s$ and while $g$ is clearly an input, $d$ and $s$ cannot be called inputs or outputs.
building a circuit from components
The following figure shows two devices connected by a wire. Connected ports must have the same value, while each device’s other ports are constrained by that device alone; We specify this by combining two formulas, identifying the connected port. Now suppose we want to hide a connected port (or any port in fact). Hiding means that the port is no longer available for connection. This is accomplished by existential quantization on the relevant variables (because some values definitely “exist”). This is exactly how relational construction is done in mathematics.
So here is a plan to verify any hardware device. We Please, specify It is specified by a formula on the variables $a$, $b$, $c$, $d$ that describe our desired behavior. We implement This is done through a circuit consisting of simple components; From the specifications of this implementation and the simple components, we obtain a formula Imp for the behavior given by the implementation (as described above). Then the formula Imp$\to$Spec expresses (for a$, $b$, $c$, $d$) that each behavior exhibited by the implementation is allowed by the specification. Now, just prove it. We can implement simple components as even simpler components for development by refinement.
Short Circuit and Other Issues
This modeling approach is obviously simple, but is it too simple? Mike called Imp$\to$Spec partial purity (which refers to correctness under the assumption of termination for software verification) because it turns into triviality in the presence of a short circuit: An implementation that connects power to ground (because then the IMP itself would be F). Although no one would intentionally create a short circuit, it is not difficult to imagine a combination of transistors that could produce a short circuit for some inputs. Given such input, the real-life implementation would melt down, but at least it wouldn’t give the wrong answer! Mike Foreman suggests addressing this issue by proving “termination” through some formula of the form $\forall\exists$Imp, claiming that Everyone The combination of “inputs” (as we consider them) can be satisfied by certain values on the remaining ports. An introductory paper devotes its final section to this issue.
Furthermore, every hardware designer can easily see that these models ignore many important design criteria: fan-out (the number of inputs that can be driven by an output), gate delay, capacitance effects, overheating. Designers must continue to rely on their other tools to deal with those issues, relying only on validation for logical functionality. Mike’s models have been good, while more detailed models like Glynn Winscale’s (incorporating signal strength) have not caught on.
In a previous post I explained some general principles about modeling. To reiterate: models approximate reality, focusing on some particular aspect (in this case, logic) about which we need to reason. Models should be simple enough that we can understand them, which also means knowing what they can’t do.
Postscript
I have written a scientific biography of Mike Gordon (also here) that outlines the history of his work on hardware verification. Interestingly, Todd Wagner also suggested using logic, but only first-order logic. Mike never mentioned Wagner to me or quoted him. And what about software verification? Mike told me that this is obviously much more difficult than in hardware, where interfaces are simpler and larger devices often have few component types that are replicated on a large scale.
<a href