; README  --  README for IHS library

===============================================================================

Notes

This directory contains an integrated ACL2 library supporting Integer
Hardware Specifications (IHS).  The premis is that integers make a good basic
data model for hardware specification and verification.  For example, a
32-bit register (or bus) can be represented as a 32-bit integer.  The library
provides facilities for dealing with both signed and unsigned integer
hardware models.  The integer model is easy to reason about (with these
libraries), and provides excellent simulation performance for specifications
created with these models. Many of the functions and lemmas were inspired by
Yuan Yu's work on the MC68020 specification done in Nqthm.

Part of the IHS library is simply a characterization of Common Lisp built-in
logical operations, e.g., LOGAND, LOGIOR, etc.  This set of primitives has
been extended with other useful operations, e.g., (LOGHEAD size i) returns
the `size' low-order bits of `i'.  Thus, 32-bit unsigned addition can be
specified as (LOGHEAD 32 (+ i j)). [ Signed addition would be
(LOGEXT 32 (+ i j)). ]

All of these books are documented!  Once INCLUDEd you can start traversing
the documentation based on the name of the book, e.g., typing "doc
logops-definitions" at the prompt:

ACL2 !>:doc logops-definitions

brings up documentation for the book "logops-definitions.lisp".  Even lemma
books are documented, try it out.

Starting at the bottom is an extension to the standard mathematics libraries.
Next up , some special theories for IHS.  Following, a generally useful book
named "quotient-remainder-lemmas.lisp".  This book characterizes FLOOR, MOD,
TRUNCATE, and REM, which are the basic mathematical functions used to reason
about fixed-length integer models of hardware.

The book "logops-definitions.lisp" is a good place to start to see what kinds
of extensions to the Common Lisp logical operations are provided.  There are
also a few very useful macro definitions, e.g., (DEFBYTETYPE WORD 32 :SIGNED)
defines a new integer type of 32-bit signed integers, recognized by (WORD-P
i).  A coercion function is also defined, e.g., any integer can be coerced to
a 32-bit signed integer simply by (WORD i).  Those interested in the highest
sped possible simulation can also have a look at LOGOPS-EFFICIENCY-HACK in
here.  Lemma support is "logops-lemmas.lisp".

To create specifications using IHS it is sufficient to simply INCLUDE the
book "ihs-definitions".  Include "ihs-lemmas" for lemma support.

Files:
======

ihs-init.lisp            --  root of the IHS library
ihs-init.acl2            --  certification script for above

ihs-theories.lisp        --  subtheories of the ACL2 boot-strap theory

math-lemmas.lisp         --  more math support for IHS

quotient-remainder-lemmas.lisp  --  theory of FLOOR, MOD, TRUNCATE, and REM

logops-definitions.lisp  --  extensions to Common Lisp logical operations
logops-lemmas.lisp       --  lemma support for logical operations

basic-definitions.lisp   --  a carved-out subset of logops-lemmas.lisp

ihs-definitions.lisp     --  a top-level book INCLUDEing the IHS definitions

ihs-lemmas.lisp          --  a top-level book INCLUDEing the IHS lemmas

ihs-doc-topic.lisp       --  top-level XDOC topic for the IHS library


==============================================================================

4-Valued Hardware Models

There is also a single book that defines and characterizes 4-valued integer
hardware models.  This library is not as complete as "logops-definitions",
but may be useful as a starting point for further development.

@logops.lisp  --  4-valued counterparts to logical operations

WARNING: Including the @logops book has a major, and potentially undesirable,
effect on the current theory.  Most functions and rules will be disabled.
Consider re-enabling some functions and rules after including @logops.

===============================================================================

Notes on theories

These books make use of various facilities in ACL2 for dealing with theories,
and there is no `right way' to do this, only strongly held opinions!  Read
the documentation in "ihs-lemmas" for IHS-LEMMAS and MINIMAL-IHS-THEORY, and
look closely at the way books are included and theories are used before
trying to do big examples with these books.  In my opinion, the best way to
use this (full) library is to:

(include-book "ihs-definitions")
(include-book "ihs-lemmas")
(minimal-ihs-theory)

If you need to, you can then ENABLE other theories as need be.

Here is an example header from a big project that used these libraries.  You
have access to all of the definitions via this library and other books
released with ACL2.

(defmacro include-library-book (book)
  "Include a book from the ACL2 distribution."
  `(INCLUDE-BOOK
    ,(concatenate 'string "/usr/local/src/acl2-sources/books/" book)))

(include-library-book "ihs/ihs-definitions")
(include-library-book "ihs/ihs-lemmas")
(include-library-book "data-structures/structures")
(include-library-book "data-structures/array1")
(include-library-book "ihs/@logops")
(include-library-book "data-structures/list-defuns")
(include-library-book "data-structures/list-defthms")
(include-library-book "data-structures/deflist")
(include-library-book "data-structures/defalist")
(include-library-book "/cli-misc/meta-lemmas")          ;Always include last!

(minimal-ihs-theory)

(in-theory (enable @logops-theory array1-lemmas meta-lemma-theory))

(enable-theory (definition-free-theory (theory 'list-defuns)))
(enable-theory (definition-free-theory (theory 'alist-defuns)))

;  Note: The IHS libraries cointain many FORCED hyps, which sometimes cause
;  problems.  These FORCEes were inserted during the original implementation
;  of these books in an old version of ACL2.  Unfortunately we have never had
;  the time to go back and get rid of them.  The temporary solution is simply
;  to disable forcing except in cases where it is absolutely needed.

(in-theory (disable (force)))
