CS 8001 Hardware Verification
Fall 2004

Tools

ACL2

Version 2.9 of ACL2 is available locally for linux machines. A version based on Gnu Common is available at ~manolios/public/acl2/v2.9-linux/gcl-saved_acl2. A version based on Allegro Common Lisp is available at ~manolios/public/acl2/v2.9-linux/allegro-saved_acl2. (The above links get you to the directories in which the ACL2 executables reside only if you are running your browser on a CoC machine.)

If you want to install ACL2, look at the ACL2 Web page for instructions. You need a common lisp compliant lisp. A free lisp that I recommend is GCL. Perhaps the easiest thing to do is to use one of the existing executables.

For Linux, use a GCL rpm to install GCL, and then installing ACL2 is easy: just follow the instructions on the ACL2 Web page.

Read appendix A of Computer-Aided Reasoning (CAR) for information on using the ACL2 system. Appendix B also contains useful information. Finally, the Hyper-Card for ACL2 Programming is a consise Web page with useful information for beginners.

Emacs

Emacs is the extensible, customizable, self-documenting real-time display editor. Most ACL2 users run ACL2 inside of an Emacs shell buffer. See Appendix A, Section A.3.5 of CAR for more information. In addition, the subdirectory emacs of the ACL2 distribution contains files (e.g., emacs-acl2.el) containing emacs commands that simplify ACL2/Emacs interaction. Emacs is available both on the Unix (/usr/local/bin/emacs) and Windows environments (in the directory C:\emacs-20.7\bin\).

Here is a version of my emacs file that has all the functions I will use in class.

GCL

ACL2 is built on top of Common Lisp compilers. GCL is a the official Common Lisp for the GNU project, therefore it is free. GCL currently compiles itself and the primary free software Lisp applications, Maxima and ACL2, on eleven GNU/Linux architectures (x86 powerpc s390 sparc arm alpha ia64 hppa m68k mips mipsel), Windows, Sparc Solaris, and FreeBSD. Locally, it is installed in the directory ~manolios/public/gcl/gcl-2.6.5.

Allegro Common Lisp

ACL2 is built on top of Common Lisp compilers. Allegro is the Common Lisp that I used to compile ACL2 locally. Allegro is a commercial product of Franz Inc. Locally, it is installed in the directory /usr/local/acl62. The executable we will use is /usr/local/acl62/alisp. HTML documentation can be accessed via the URL /usr/local/acl62/doc/introduction.htm.

Last modified: Tue Oct 19 19:55:36 EDT 2004