Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item:

This item has been viewed 13 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-93-268.dviTeX DVI file775.26 kBTeX dviView/Open
ECS-LFCS-93-268.PDFAdobe PDF14.02 MBAdobe PDFView/Open
ECS-LFCS-93-268.psPostScript file1.25 MBPostscriptView/Open
Title: Embedding Hardware Description Languages in Proof Systems
Authors: Goossens, Kees G W
Supervisor(s): Anderson, Stuart
Fourman, Michael
Issue Date: Jul-1993
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: The aim of this thesis is to investigate the integration of hardware description lamguaages (HDLs) and automated proof systems. Simulation of circuit designs written in an HDL is an important method of testing their correctness. However, due to the combinatorial explosion of possible inputs it is not feasible to verify designs using simulation alone. Formal hardware verification, using a proof system, has tried to address this issue. Whilst some medium-sized designs have been (partially) verified, industrial take-up of formal methods has been slow. This is partly due to the use of specialised, non-standard notations employed in various formalisms. By embedding a hardware description language in a proof system we hope to clarify the semantics of the particular HDL, and present a more standard interface to formal methodologies. We have given a new static structural operational semantics for a subset of the ELLA hardware language. The formal dynamic semantics of this subset is based on an existing informal model. We embedded the semantics of this HDL in the LAMBDA higher-order logic proof system. The embedding allows meta-theoretical results to be proved about this and other semantics. It has been proved that the semantics computes the least fixed point solution of the circuit description. Another semantics which computes a more defined output has also been embedded, and the relationship between both semantics has been proved formally. A number of paradigms such as operational semantics based formal symbolic simulation, formal interactive (top-down and bottom-up) synthesis, formal hardware generators, proved correct transformations and traditional hardware verification are presented as small case studies. However, scaling up of the examples turned out to be difficult and verification tended to be slow.
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy