Centaur Books

Introduction

The Centaur Books are a free set of ACL2 libraries for formal hardware verification including:

VL — a Verilog parser and simplification tool.
E — a deeply embedded hardware description language with a well-defined semantics.
ESIM — a symbolic simulator for E modules.
GL — a symbolic simulator for ACL2 functions and framework for bit-blasting ACL2 theorems.
Many supporting libraries, e.g., for representing Boolean or four-valued logic expressions, debugging ESIM runs with waveforms, reasoning about arithmetic, and so forth.

Centaur Technology is a small company in Austin, TX. We design x86 processors for our parent company, VIA Technologies. We have used these books to prove correctness properties of several execution units, and to develop other tools such as an equivalence checker, a linter, etc.

Warning: you are welcome to use these books, but you should expect them to be much less stable than ordinary ACL2 books; we are actively using them and often need to extend them.

Prerequisites

Recommended Hardware: You will at least want a fast dual-core machine with 8 GB of memory. Having additional cores is very useful for quickly re-certifying books in parallel, but careful here: with more cores you'll need even more memory to avoid swapping death. A good target might be at least 4 GB per core.; We used to recommend even more memory than this. Ample memory was especially important when we carried out large proofs using BDDs, but these days we often use SAT instead, and SAT is far less memory intensive. Even so, today many of our real hardware proofs are made faster (or possible) by having 32 or more GB of memory. Also, many of our tools, e.g., our Verilog parser, are written in a memory-hungry way because that's just the kind of environment we work in.
Recommended Operating System: We use 64-bit Linux. Other unix derivatives like Darwin, FreeBSD, etc., might work reasonably well, but Linux is our main platform. Windows probably won't work, although a Linux VM inside of Windows may be a fine option. You will need ordinary tools like perl, make, etc.
Clozure Common Lisp Configuration: We use 64-bit Clozure Common Lisp. Other Lisps probably won't work.; We usually use a fairly recent SVN snapshot.; CCL Configuration before building ACL2: We use ccl-config.lsp to do some extra configuration that increases the stack sizes and tunes the garbage collector for better performance.; We configure our PATH so that we can run CCL by typing ccl.
ACL2 Configuration: We configure our PATH so that we can run ACL2(h) by typing acl2.
cert.pl Configuration: We generally use cert.pl to certify books. This script is located in the acl2/books/build directory.; We configure our PATH so that we can run cert.pl by typing cert.pl. Note that other useful scripts like critpath.pl are also in the acl2/books/build directory.
(Optional) GTKWave Configuration: You can skip this if you aren't doing hardware verification.; We often use GTKWave for debugging waveforms. Other VCD file viewers may also work.; We configure our PATH so that we can run GTKWave by typing gtkwave.
(Optional) Sat Solver Configuration: We often use various SAT solvers in conjunction with GL. See SAT-SOLVER-OPTIONS for details about installing a suitable SAT solvers.

Building the Books

Once you have the above prerequisites, you will be ready to certify the ACL2 books. We prefer to do this via:

$ # install prerequisites as explained above
$ cd [...]/acl2/books/
$ make USE_QUICKLISP=1 -j 4 centaur manual   # -j 4 for a quad-core processor

The USE_QUICKLISP=1 instructs make to enable support for Quicklisp, which is necessary for certain books.

Depending on your hardware this may take ten minutes up to hours. For reference, it takes about an hour on an 8-core AMD-FX8350 with 32 GB of memory running FreeBSD, using -j 8.

Next Steps

The make command above should produce the usual ACL2+Books manual which covers the Centaur books and also has the regular documentation for ACL2 and other Community Books like arithmetic, std, etc.

To view the manual, point your web browser at acl2/books/doc/manual/index.html—this link will be broken until you generate the manual.

(Matt Kaufmann typically maintains a fairly recent version of the manual at the UT web site, so you may usually not need to build a local copy yourself.)

If you are specifically interested in hardware verification, there is also a preliminary tutorial that walks through the verification of a trivial ALU module. To get started, see:

books/centaur/esim/tutorial/intro.lisp

Contact Information

Unfortunately we can't offer any serious technical support. We may be able to answer some questions on an informal, "low bandwidth" basis, in our spare time.

We ask that you send any technical questions, comments, or bug reports about these books to the acl2-help or acl2-books lists.

If for some reason that is not appropriate, you can send email directly to Jared Davis and Sol Swords, {jared,sswords}@centtech.com.

License Information

Contact Information: Centaur Technology Formal Verification Group
7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
http://www.centtech.com/
License: (An MIT/X11-style license): Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:; The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.