Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Single-Threaded Processor Models: Enabling Proof and High-Speed Execution

Multiple device models are routinely built during processor development. Because ACL2's logic is a subset of a real programming language (Common Lisp) it can be used to construct models that support both simulation and analysis. Although reducing the number of processor models to be built and maintained is itself valuable, even more important is the potential use of standard development practices that rely on simulation to validate the model that is used for formal analysis. Providing rapid execution for simulators written in ACL2 is critical for ACL2's use in building real processor simulators.

This talk describes a hypothetical, simple processor TINY and presents various methods for writing its interpreter in ACL2. Comparison of the various TINY models presented illustrates how inefficiency usually associated with applicative program execution can be overcome, and how this execution optimization can be justified by ACL2.

Slides

Examples

Matt Wilding