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 .
To obtain the FM9001 system, use anonymous ftp . Then follow the instructions of this README.
Bishop C. Brock and Warren A. Hunt, Jr.
brock@cli.com, hunt@cli.com