CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

Project 1, Due 10/6/2002 (before midnight)

Note: Make sure that you allocate enough time to the project. As a rough guideline, I suggest that you complete parts 1 and 2 below by September 25.

  1. ACL2 Warm Up. Read chapters 3, 4 (section 4.6 is optional), and 5 of CAR (Computer-Aided Reasoning) and check your understanding by doing the exercises as you go. Hand in your solutions to the exercises below. The exercises must be done with ACL2, that is, test your solutions using the ACL2 system (instructions on how to access ACL2 locally appear here).
  2. Modeling processors in ACL2. We will use ACL2 to model processors. Once you go through the above intro to ACL2, you are ready to read the following paper which describes the general approach.

    Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. A pdf version is also available.

    This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called "small machine" model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models.

    Read up to the end of section 4.4 carefully and briefly skim the rest of the paper.

    An ACL2 file with the relevant definitions can be found here.

    Notice that what we have is a simulator for the small machine and what is interesting about the paper is that it then goes on to describe how one can state, prove, and mechanically verify theorems about the simulator.

    Write a pair of functions fact-program and fact-clock so that for any natural number, n

    (equal (car (mem (sm (fact-state n)
    		     (fact-clock n))))
           (fact n))
    is a theorem, where fact and fact-state are defined as follows.
    (defun fact (n)
      (if (zp n)
        (* n (fact (1- n)))))
    (defun fact-state (n)
      (st :pc   '(fact . 0)
          :stk   nil
          :mem  `(,n)
          :halt nil
          :code (list (times-program) (fact-program))))
    That is, (sm (fact-state n) (fact-clock n)) is a state with a memory whose first element is n! (n factorial). Times-program and the other functions appearing in the above expression are in the ACL2 file mentioned above. Try your solution with the following values for n: 7, 15, 22. You may have to compile your definitions if you run into stack overflows (type (comp t) at the command prompt). If your solutions are correct, then ACL2 should prove theorems of the following form (automatically).
    (defthm fact-theorem-7
      (equal (car (mem (sm (fact-state 7)
                           (fact-clock 7))))
             (fact 7)))

    For this part of the project, submit your definitions of the functions fact-program and fact-clock and defthms fact-theorem-7, fact-theorem-15, fact-theorem-22, where fact-theorem-7 is as above and the other defthms are the same, except occurences of 7 are replaced by 15 and 22.

  3. A JVM-like processor in ACL2. This part of the project requires that you write two simulators for JVM-like languages. The first simulator describes a JVM-like language at a higher level of abstraction than the second. The simulators will act as specifications for the machine we build on hardware.
    1. First we examine bit vectors in ACL2. This is important because the arithmetic and logical operations of our JVM-like machines are on 32-bit numbers. Read about bit-vectors here.
    2. The first JVM-like machine is called the iJVM. The specification of the iJVM along with instructions on what you have to submit can be found here.
    3. The second JVM-like machine is called the iJVM2. The specification of the iJVM2 along with instructions on what you have to submit can be found here.
    4. Optional: Characterize the relationship between the two simulators. Here are some suggestions:
      • Try to do this precisely using English.
      • What theorem would you prove relating the two?
      • Write a compiler in ACL2 from iJVM to iJVM2. What does it mean for the compiler to be correct?

    Sumbission Instructions

    Create an archive of the files using tar or winzip (if you want to use something else, ask first to make sure we can unarchive it) and send us the archive (as a single attatchement) via email. The email should be sent both to me and to Vernard (vernard@cc).