Show simple item record

dc.contributor.advisorAnderson, Stuart
dc.contributor.advisorFourman, Michael
dc.contributor.authorGoossens, Kees G W
dc.date.accessioned2004-03-03T15:25:08Z
dc.date.available2004-03-03T15:25:08Z
dc.date.issued1993-07
dc.identifier.urihttp://hdl.handle.net/1842/408
dc.description.abstractThe 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.en
dc.format.extent793864 bytes
dc.format.extent14353059 bytes
dc.format.extent1284401 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleEmbedding Hardware Description Languages in Proof Systemsen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record