## The Formalisation of a Hardware Description Language in a Proof
System: Motivation and Applications

**K G W Goossens**
*Abstract:* Hardware description languages (HDLs) are a
notation to describe behavioural and structural aspects of circuit
designs. We discuss why it is worthwhile to give a formal semantics
for an HDL, and why we have encoded such a semantics in a proof
system. We outline the subset of the hardware description language
ELLA which we use, its formal structural operational semantics, and
its embedding in the higher-order logic proof system LAMBDA.
Finally we discuss applications of this approach which include the
ability to prove results about the simulation mechanism, formal
symbolic simulation, various synthesis techniques, and
transformational design.

*LFCS report ECS-LFCS-93-269, June 1993.*

This report is available in the following formats:

Previous |

Index |

Next