Embedding Hardware Description Languages in Proof Systems

                        K G W Goossens

The aim of this thesis is to investigate the integration of widely used
hardware description languages ({\sc hdl}s) and automated proof systems.

Simulation of circuit designs written in an {\sc hdl} is an important
method of testing their correctness.  However, due to the combinatorial
explosion 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 {\sc hdl}, and present a more
standard interface to formal methodologies.  We have given a new static
structural operational semantics for a subset of the {\sc ella} hardware
description language.  The formal dynamic semantics of this subset is based
on an existing informal model.

We embedded the semantics of this {\sc hdl} in the {\sc Lambda} higher
order logic proof system.  The embedding allows meta-theoretical results to
be proven about this and other semantics.  It has been proven that the
semantics computes the least fixed point solution of the circuit
description.  Another semantics which computes a more optimal output has
also been embedded, and the relationship between both semantics has been
proven formally.

A number of paradigms such as operational semantics based formal symbolic
simulation, formal interactive (top-down and bottom-up) synthesis, formal
hardware generators, proven 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.