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