SECD: THE DESIGN AND VERIFICATION OF A FUNCTIONAL MICROPROCESSOR

Date
1990-06-01
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The subject of this thesis is a silicon implementation of Landin's SECD machine. The starting point was an abstract specification defined by instruction transitions. Work completed includes the evolution of the design by transformation from the abstract specifications down to microcode, laying out the design in silicon, and the formal verification of its functional correctness using the HOL proof assistant. A top level specification for the SECD system as well as an implementation level definition are generated using the HOL system. The intended operating conditions are formally defined, and installed as constraints in a machine-assisted proof of correctness stating that the computation effected by the implementation model meets the specification. The specification raises issues of the representation of S-expression data structures with destructive operation on shared structures. A solution which defines an abstract memory data type which can embed the data structures is used in the formal specification. Several issues related to the representation of temporal aspects of the chip function are analysed. The SECD chip is one of the most complex devices subjected to formal verification to date, and is unique in combining the design and layout with the formal specification and verification of an integrated circuit. The problem size prevents presentation of either the specification or proof in their entirety, however techniques used to manage the inherent complexity are presented in conjunction with a representative sampling of the specifications and proofs.
Description
Keywords
Computer Science
Citation