[T5] ================================================ AMAST Links 02 07

                      The FM9001 Microprocessor:
      Its Formal Specification and Mechanical Correctness Proof

  We are releasing the mechanically checked proof scripts for the
FM9001 microprocessor.  The FM9001 is a general-purpose 32-bit
microprocessor which has been implemented as a CMOS ASIC.  The proof
being released rigorously connects the expression of the FM9001 as a
netlist with the characterization of the FM9001 at the machine-code
programmer's level.  (The FM9001 is the foundation of the `CLI Stack',
which also includes several verified compilers and applications all
running on the FM9001.  Other parts of the `CLI Stack' are separately
released.)
  To obtain information about the FM9001 microprocessor and proof,
please examine the WWW page at URL:
http://www.cli.com/hardware/fm9001.html
  To obtain the FM9001 system, use anonymous ftp from URL:
ftp://ftp.cli.com/pub/fm9001/README
Then follow the instructions of this README.

   Bishop C. Brock and Warren A. Hunt, Jr.
   brock@cli.com, hunt@cli.com