Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05197-0@swan.cl.cam.ac.uk>; Tue, 18 Aug 1992 13:15:37 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10666; Tue, 18 Aug 92 05:07:29 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA10661; Tue, 18 Aug 92 05:07:21 -0700 Received: from puffin.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <05005-0@swan.cl.cam.ac.uk>; Tue, 18 Aug 1992 13:06:03 +0100 To: info-hol@edu.uidaho.cs.ted (info-hol mailing list) Subject: Book Announcement Date: Tue, 18 Aug 92 13:05:58 +0100 From: Brian Graham Message-Id: <"swan.cl.ca.007:18.07.92.12.06.06"@cl.cam.ac.uk> The following may be of some interest to users of HOL and formal methods in hardware verification in general. ========================================================================== The SECD Microprocessor A Verification Case Study by Brian T. Graham, University of Calgary and University of Cambridge The SECD Microprocessor is a substantial case study in hardware specification and verification. The subject is a silicon implementation of Landin's SECD machine, which is transformed into a layout, formally specified, and partially verified using the HOL proof assistant. It is important as a nontrivial worked example, clearly describing the organization and execution of the correctness of proof, and by making the sources available, will be helpful to those considering the use of or learning about the application of formal methods. The architecture is designed to provide support for functional programming, with complex machine instruction semantics to support recursive definitions and function calls. This considerably raises the complexity of the state transitions to be verified, and an abstract data type and operations are introduced to express the specification. The SECD Microprocessor illustrates what formal methods can achieve today, not only by some expert elite, but by anyone prepared to carefully consider the problems at hand. 1992, 192 pp. Hardbound, US $62.50/Dfl. 135.00/GB 40.50 ISBN 0-7923-9245-0 The Kluwer International Series in Engineering and Computer Science 178 Table of Contents Foreword Preface 1. Formal Methods and Verification 2. LispKit and the SECD Architecture 3. SECD Architecture: Silicon Synthesis 4. Formal Specification of the SECD Design 5. Verification of the SECD Design 6. Denouement Bibliography Index ========================================================================== The following ordering information is provided by the publisher. The book is available from both the European and North American offices. Europe: KLUWER ACADEMIC PUBLISHERS GROUP Order Dept. P.O. Box 322 3300 AH Dordrecht, The Netherlands Fax +31-78-524474. email: mckluwer@kap.nl Orders from individuals accompanied by payment or authorization to charge a credit card account will ensure prompt delivery. Postage and handling charges will be absorbed by the Publisher on all such orders. Payment will be accepted in any convertible currency. Please check the rate of exchange at your bank. For sales within the Netherlands please add 6% VAT (BTW). Prices are subject to change without notice. North America: Kluwer Academic Publishers 101 Philip Drive Norwell, MA 02061 tele: (617) 871-6600 ------------------------------------------------------------------------------ Brian Graham | Tel: +44-223-334688 University of Cambridge | Fax: +44-223-334678 Computer Laboratory | Pembroke Street | Email: btg@cl.cam.ac.uk Cambridge, U.K. CB2 3QG |