|
|
An Equational Approach to the Verification of MicroprocessorsThis paper develops a method for formally proving the correctness of a microprocessor using an equational approach. The behavioral and structural specifications of the processor are expressed in a functional language with an equational semantics. The specification defines the effect of a single macroinstruction at the abstract level and a single microinstruction at the structural level. One of the difficulties in specifying and verifying the design using a ``non-temporal'' formalism such as equational logic (in which timing is not modelled explicitly) lies in characterizing and reasoning about the ``asynchronous'' interactions that may take place between the CPU and other modules, such as the memory module. Consequently, most previous works using a functional approach did not take these asynchronous interactions into account. Other works modelled asynchrnous interactions, but had to encode the asynchronous interactions in a deterministic fashion using artifacts such as an ``oracle,'' which complicated the proofs. In contrast, our specification captures the asynchronous handshake interaction between the memory and the CPU directly by modelling memory as an independent module that processes read/write requests to an array-like store. Our correctness criterion is specified as a formula in first-order logic (with existential quantifiers), which, together with a notion of a global clock, enables us to prove safety and liveness conditions about these asynchronous interactions. This makes our specification more direct and natural than previous efforts based on functional formalisms. A general correctness criterion is formulated as a sentence in first-order predicate calculus with equations relating expressions of the specification language as atomic literals. To apply the criterion to a particular design, one must additionally define (1) an abstraction function that relates the concrete and the abstract representations of the state of the microprocessor, and (2) an invariant condition that must be true of the processor state at the start of every instruction cycle. The basic technique used in the verification is equational simplification of expressions, augmented with familiar proof strategies such as instantiation, case-splitting, and induction. The method is first illustrated by applying to a simple, hypothetical microprocessor, and then used to verify a more complex design based on the microprocessor used in the Lilith Modula II machine. |
|
Maintained by Sekar, sekar@cs.sunysb.edu |