Overview

""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 progamming, 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 an expert, but by anyone prepared to carefully consider the problems at hand.

Full Product Details

Author:   Brian T. Graham
Publisher:   Springer
Imprint:   Springer
Edition:   1992 ed.
Volume:   178
Dimensions:   Width: 15.50cm , Height: 1.20cm , Length: 23.50cm
Weight:   1.000kg
ISBN:  

9780792392453

ISBN 10:   0792392450
Pages:   176
Publication Date:   31 May 1992
Audience:   College/higher education ,  Professional and scholarly ,  Postgraduate, Research & Scholarly ,  Professional & Vocational
Format:   Hardback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

1 Formal Methods and Verification.- 1.1 Achievements in Hardware Verification.- 1.2 The HOL System.- 2 LispKit and the SECD Architecture.- 2.1 The Syntax of LispKit.- 2.2 The Interpretation of LispKit.- 2.3 SECD Architecture.- 2.4 LispKit to SECD Machine Code.- 2.5 Summary.- 3 SECD Architecture: Silicon Synthesis.- 3.1 Project Context.- 3.2 Levels of the Design.- 3.3 The Chip Interface.- 3.4 Internal Architecture and Microcode.- 3.5 The Final Layout.- 3.6 Summary and Status.- 4 Formal Specification of the SECD Design.- 4.1 Modelling Hardware.- 4.2 The Top Level Specification.- 4.3 The Low Level Definition.- 4.4 Register Transfer Level Specification.- 4.5 Relating the Levels.- 4.6 Summary.- 5 Verification of the SECD Design.- 5.1 Constraints.- 5.2 Structure of the Proof.- 5.3 Unfolding the System Definition.- 5.4 Phase Stage: Effect of Each Microinstruction.- 5.5 Microprogramming Stage: Symbolic Execution.- 5.6 Liveness.- 5.7 Computations across abstraction.- 5.8 Summary.- 6 Denouement.- 6.1 Putting the Proof Result into Context.- 6.2 Retrospective Improvements.- 6.3 Hardware Verification.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions