The SECD Microprocessor
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 or learning...
Search in google:
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 or learning about the application of formal methods. The architecture is designed to provide support for functional programming, with complex machine instruction 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. Booknews A case study in hardware specification and verification, using the nontrivial worked example of a silicon implementation of Landin's SECD machine, which is transformed into a layout, formally specified, and partially verified using the HOL proof assistant. The study shows that large and complex verifications can be carried out by people without a lot of experience if they are willing to pay attention to procedures and details. Annotation c. Book News, Inc., Portland, OR (booknews.com)
ForewordPreface1Formal Methods and Verification11.1Achievements in Hardware Verification31.2The HOL System42LispKit and the SECD Architecture92.1The Syntax of LispKit102.2The Interpretation of LispKit132.3SECD Architecture232.4LispKit to SECD Machine Cods272.5Summary313SECD Architecture: Silicon Synthesis333.1Project Context333.2Levels of the Design343.3The Chip Interface363.4Internal Architecture and Microcode383.5The Final Layout513.6Summary and Status534Formal Specification of the SECD Design574.1Modelling Hardware594.2The Top Level Specification604.3The Low Level Definition704.4Register Transfer Level Specification734.5Relating the Levels934.6Summary975Verification of the SECD Design1015.1Constraints1025.2Structure of the Proof1095.3Unfolding the System Definition1115.4Phase Stage: Effect of Each Microinstruction1175.5Microprogramming Stage: Symbolic Execution1205.6Liveness1355.7Computations across abstraction1375.8Summary1536Denouement1576.1Putting the Proof Result into Context1596.2Retrospective Improvements1636.3Hardware Verification165Bibliography169Index175
\ BooknewsA case study in hardware specification and verification, using the nontrivial worked example of a silicon implementation of Landin's SECD machine, which is transformed into a layout, formally specified, and partially verified using the HOL proof assistant. The study shows that large and complex verifications can be carried out by people without a lot of experience if they are willing to pay attention to procedures and details. Annotation c. Book News, Inc., Portland, OR (booknews.com)\ \
