Index of /users/moore/acl2/current/distrib/acl2-sources/books/workshops/1999/simulator

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                20-Jul-2009 18:13  359   
 exercises.lisp          13-Oct-2008 14:04   10K  
 tiny.lisp               13-Oct-2008 14:04   31K  

This directory contains two files of ACL2 input associated with
"High-Speed Analyzable Simulators", Chapter 8 of the Kluwer Academic
book "Computer-Aided Reasoning: ACL2 Case Studies".

tiny.lisp	  The toy machine "TINY" used for illustration in 
                  the chapter, and a proof of a small TINY program

exercises.lisp    Solutions for each of the chapter exercises

Some of the methods implicit in these files, as well as our
motivation, a description of the toy processor, and an indication of
how we apply these techniques on real processors, are documented in

  M. Wilding, D. Greve, D. Hardin, "Efficient Simulation of Formal
  Processor Models" 1998.  (To appear in Formal Methods in System
  Design in 2000; original TR available at pobox.com/~hokie/docs.)


David Greve and Matt Wilding
April 2000