SECD: THE DESIGN AND VERIFICATION OF A FUNCTIONAL MICROPROCESSOR
Date
1990-06-01
Authors
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