Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 17 Aug 1995 19:32:46 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id NAA22410 for qed-out; Thu, 17 Aug 1995 13:21:58 -0500 Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP id MAA21161 for ; Thu, 17 Aug 1995 12:13:59 -0500 Received: from dilbert.cli.com by cli.com (4.1/SMI-4.1) id AA28064; Thu, 17 Aug 95 12:13:25 CDT From: hunt@CLI.COM (Warren A. Hunt Jr.) Received: by dilbert.cli.com (4.1) id AA27976; Thu, 17 Aug 95 12:13:25 CDT Date: Thu, 17 Aug 95 12:13:25 CDT Message-Id: <9508171713.AA27976@dilbert.cli.com> To: qed@mcs.anl.gov Subject: FM9001 Release Announcement Sender: owner-qed@mcs.anl.gov Precedence: bulk The FM9001 Microprocessor: Its Formal Specification and Mechanical Correctness Proof Summer 1995 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 URL http://www.cli.com/hardware/fm9001.html To obtain the FM9001 system, connect to Internet site ftp.cli.com by anonymous ftp, giving your email address as the password, `get' the file /pub/fm9001/README and follow the instructions therein. Or get the URL ftp://ftp.cli.com/pub/fm9001/README via your WWW browser. Bishop C. Brock and Warren A. Hunt, Jr. brock@cli.com hunt@cli.com