Anderson, Stuart

Fourman, Michael

Goossens, Kees G W

2004-03-03T15:25:08Z

2004-03-03T15:25:08Z

1993-07

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.

793864 bytes

14353059 bytes

1284401 bytes

application/x-dvi

application/pdf

application/postscript

http://hdl.handle.net/1842/408

en

University of Edinburgh. College of Science and Engineering. School of Informatics.

Embedding Hardware Description Languages in Proof Systems

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy