ACL2 Script for
Symbolic Simulation: An ACL2 Approach

J Strother Moore


Executable formal specification can allow engineers to test (or simulate) the specified system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation, the ``execution'' of the formal specification on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes the working engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal specification of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet.

The full paper refers to an ACL2 script containing an ACL2 model of a ``small machine.''

The ``small machine'' model discussed in this paper was first developed in 1991 for a course on how to use the Boyer-Moore theorem prover, Nqthm, to model microprocessors. The Nqthm model is a distillation of the microprocessor modeling approach developed by the Nqthm community at the University of Texas at Austin and Computational Logic, Inc., in the 1980s. The small machine model was transcribed to ACL2 in 1995 and described in the paper:

That paper also has an accompanying ACL2 Script.

Thus, there are two ACL2 scripts formalizing the small machine, the 1996 one and the present one (1998). They are different! The differences stem from the fact that the 1996 model was not Common Lisp compliant. In order to do the performance measuring reported in the present paper, I decided to change the model to make (and prove) it compliant. I list the differences between the two models below.