SECD: THE DESIGN AND VERIFICATION OF A FUNCTIONAL MICROPROCESSOR

Simple item page
dc.contributor.authorGraham, Brian T.eng
dc.date.accessioned2008-05-20T23:28:50Z
dc.date.available2008-05-20T23:28:50Z
dc.date.computerscience1999-05-27eng
dc.date.issued1990-06-01eng
dc.description.abstractThe 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.eng
dc.description.notesWe are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.caeng
dc.identifier.department1990-395-19eng
dc.identifier.doihttp://dx.doi.org/10.11575/PRISM/31358
dc.identifier.urihttp://hdl.handle.net/1880/46522
dc.language.isoEngeng
dc.publisher.corporateUniversity of Calgaryeng
dc.publisher.facultyScienceeng
dc.subjectComputer Scienceeng
dc.titleSECD: THE DESIGN AND VERIFICATION OF A FUNCTIONAL MICROPROCESSOReng
dc.typeunknown
thesis.degree.disciplineComputer Scienceeng
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
1990-395-19.pdf
Size:
10.74 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Plain Text
Description:
Download
Collections
Science Research & Publications