Examples of other models and proof techniques
The topic operational-semantics-1__simple-example deals with a simple machine, M1, and focuses on the “clock”-based proof style. In this section we point to other machine models, different ACL2 proof styles, and tools in the ACL2 Community Books that may be of interest.
We limit our discussion here to operational semantics. But it is worth
noting that a valuable way to explore the diversity of ACL2 applications and
extensions is to browse the ACL2 Workshop series. See the “ACL2
Workshops, UT Seminar, and Course Materials” link on the ACL2 homepage. Then
visit the Program for each workshop. Many of the papers include supplemental
material in the form of ACL2 proof scripts are in the ACL2 Community Books
regression suite and thus available locally if you've installed ACL2.
They're under the directory
As noted in operational-semantics-5__history-etc, a “handheld calculator” was formalized in Chapter 17 bib::bm79, using the precursor to Nqthm. That machine was essentially M1 without the branch or jump instructions. That is, all programs were just straightline sequences of stack-based arithmetic operations. The Bendix 930 flight control computer discussed in bib::bm80 was a more traditional von Neumann machine, also modeled in the precursor to Nqthm. The 30 page model is listed in Section 15 of bib::bm80.
The Computational Logic, Inc. (CLI) Verified Stack was formalized and verified with Nqthm. The CLI Verified Stack was a hardware-software stack consisting of a gate-level description of a microprocessor, its instruction set architecture, an assembler/linker/loader for a stack based assembly language with subroutine call and return, a compiler for a simple subset of a Pascal-like language, a simple operating system kernel, and some applications programs. Each component of the stack was verified with respect to the component immediately below in such a way that the correctness theorems could be composed. The result was that if a program in the high-level language was verified (with respect to the operational semantics of the high-level language) then compiling, assembling, linking, and loading the binary image onto the gate-level machine and running it would, with mathematical certainty, deliver the results verified at the high level. The stack was described in the 1989 special issue of the Journal of Automated Reasoning, bib::bhmy89. In 1992, a hardware description language was formalized and another microprocessor was described and verified to implement a slightly different machine code. That microprocessor was fabricated, the assembler/linker/loader was retargeted to the new machine code and verified, so that the entire stack was then ported to a fabricated microprocessor. A second compiler (for a Lisp subset) and a game-playing applications program were also written and verified. The CLI Stack was a project by Bill Bevier, Bishop Brock, Art Flatau, Warren A. Hunt, Jr., Matt Kaufmann, J Moore, Matt Wilding, and Bill Young, of Computational Logic, Inc.
The CLI Verified Stack convinced us that this style of operational semantics was viable not just for program verification but for stacking and relating machines. For more details, including papers, books, dissertations, and proof scripts, start at the annotation for bib::bhmy89 and visit the citations.
[Personal aside by Moore: I believe the CLI Verified Stack to be a seminal achievement in formal methods.]
The most elaborate machine model created with Nqthm was of the Motorola
MC68020, modeled by Yuan Yu bib::yu92. He and Boyer used that model
to verify many MC68020 machine code programs produced by a variety of
standard compilers. Perhaps most notably they verified the machine code for
Hoare's Quick Sort and 21 of the 22 functions in the Berkeley Unix C string
library (as compiled with
Of course, state machines are not limited to modeling computational
engines. See bib::bgm90 for a real-time control problem formalized
with a “clocked” state machine where the “clock”
specifies the change in the physical environment at each sampling cycle. In
addition, games can often be formalized with state machines where the
“clock” specifies opponents' moves. Strategies can be analyzed
via proof. See the Nqthm script analyzing the game of Tic Tac Toe,
But for the rest of this discussion we focus on modeling and proving properties of compute engines with ACL2.
The first major external applications of ACL2 after it was developed at Computational Logic, Inc., were at Motorola Government Systems, in Scottsdale, Arizona, between 1993 and 1997, and at Advanced Micro Devices, Inc. (AMD), in Austin, Texas, in 1995. Only the first of these two projects employed operational semantics — and it was a tour de force.
A CLI employee, Bishop Brock, relocated to Scottsdale and embedded with a design group there to formalize the evolving design of the Motorola “Complex Arithmetic Processor” (CAP) digital signal processor (DSP), using the operational semantic techniques developed with Nqthm and described above. A timeline of the entire ACL2 part of the CAP DSP project may be found in bib::bkm96.
Here is a brief description of the CAP design taken from Section 2.1 of bib::bkm96.
The CAP design follows the `Harvard architecture', i.e., there are separate program and data memories. The design includes 252 programmer-visible data and control registers. There are six independently addressable data and parameter memories. The data memories are logically partitioned into `source' and `destination' memories; the sense of the memories may be switched under program control. The arithmetic unit includes four multiplier-accumulators and a 6-adder array. The CAP executes a 64-bit instruction word, which in the arithmetic units is further decoded into a 317-bit, low-level control word. The instruction set includes no-overhead looping constructs and automatic data scaling. As many as 10 different registers are involved in the determination of the next program counter. A single instruction can simultaneously modify well over 100 registers. In practice, instructions found in typical applications simultaneously modify several dozen registers. Finally, the CAP has a three-stage instruction pipeline which contains many programmer-visible pipeline hazards.
Brock, with help from Warren Hunt, J Moore, and Matt Kaufmann, developed a bit- and cycle-accurate model of the CAP design. We believe this was the first time an entire commercial microprocessor was formally specified, see bib::bh99.
Brock validated the design by running the ACL2 model against Motorola's SPW engineering model of the processor. For example, he compared the results of executing an end-to-end application (a QPSK modem) on both the SPW model and the ACL2 model and found the final states bit-exact for all programmer visible registers.
Before turning to the verification of CAP applications programs Brock undertook the logical elimination of the CAP pipeline. He defined a predicate that syntactically detected pipeline hazards in microcode and he implemented a simpler ACL2 machine model without the pipeline. Then, following Burch and Dill's method of comparing states after flushing the pipeline via symbolic evaluation, he proved with ACL2 that the two models were equivalent provided the microcode was hazard free.
Then Brock, et al, proved several microcode programs correct, again
following the proof methodology we sketched in section “Proving
Theorems about M1 Programs” of
It is noteworthy that ACL2 executed the pipeline-free microcode interpreter several times faster than the hardware simulator could execute the SPW model — with assurance that the answers were equivalent to the pipelined model on hazard-free microcode. In addition, the ACL2 hazard predicate, being an executable ACL2 function on microcode programs, was executed on over fifty microcode programs written by Motorola engineers and extracted from the ROM mechanically. Hazards were found in some of these. See bib::bh99. This can be considered another practical application of formal methods since the hazard detection predicate was formally verified to be a sufficient condition for the pipelined and non-pipelined machines to be equivalent.
Unfortunately, Motorola canceled the entire CAP effort before the device was fabricated, despite the success of the formal methods component of the project. The ACL2 proof scripts are not in the ACL2 Community Books regression suite.
We now move on to other operational models. In operational-semantics-1__simple-example (and on the ACL2 directory
The use of the inductive assertion method with an operational semantics of this style is quite interesting. As noted in bib::mmrv06, no other tools are required beyond the operational semantics and a theorem prover. It is possible for the theorem prover to use the operational semantics directly to generate and prove the “verification conditions” one gets by exploring all possible program paths between assertions in the code. One can use the method to prove either partial or total correctness, the former meaning “correct if it terminates” and the latter meaning “terminating and correct at termination.”
The most complicated machine formalized (as of 2024) with ACL2 is the x86
instruction set architecture. The model evolved from simpler models,
exploiting lessons learned from earlier Nqthm and ACL2 work. In the case of
x86, the “toy” was the y86 as informally described in bib::boh03. The ACL2 directory
From the y86, the model of the x86 evolved through several iterations reported in bib::hk12, bib::ghk13, and bib::ghkg14, to Shilpi Goel's monumental x86 model bib::goel16 and bib::ghk17. The model specifies over 400 x86 instructions and the model includes architectural features like segmentation and paging. It can be executed in either of two modes. When running in the application-program level, it executes about 3.3 million x86 instructions per second. When running in the system-level mode it executes about 912,000 x86 instructions per second. The model has been validated extensively against actual x86 hardware, which is the reason so much attention has been paid to execution efficiency. X86 machine code programs have been verified. See bib::goel16 and bib::ghk17.
The paper bib::moore99b shows how we can reason about a system involving multiple processes interacting with a shared memory. The paper describes two operational models, one in which the model switches between multiple processes according to an “oracle” and the other which models just a single process but in which the memory changes “spontaneously.” The two models are then related by proved lemmas so that one can switch back and forth between views. The lemmas are used to verify a safety property (using one model) and a progress property (using the other). All the proofs are carried out via the clock-based methodology.
We have focused on the clock-based proof methodology. But an advantage of creating “toy” models is that it is easy to explore other proof methodologies and then try to apply them to larger models.
The papers bib::rm04 and bib::rhmm07 establish that the clock-function approach to verification is equivalent to the use of inductive assertions and to stepwise invariants. In fact, ACL2 tools are provided for converting between clock-based proofs and inductive assertion-style proofs.
The paper bib::sawada00 describes the modeling and verification of a pipelined machine. The paper bib::manolios00 shows an alternative method based on Well-founded Equivalence Bisimulations. Briefly, it introduces a notion of correctness that implies that the instruction set architecture and micro-architecture machines have the same observable infinite paths, up to stuttering.
The paper bib::sh98 deals with a machine with precise exceptions and speculative execution.
An ACL2 tool to help manage states in operational models is described in
bib::moore15 and a tool for determining whether two symbolic terms
representing machine addresses may be equal is described in bib::moore17. These tools are available among the ACL2 Community Books. A
tool for deriving the meaning of and clock function for a piece of code from
the code and the operational semantics model is described in the ACL2 file