The Formalisation of a hardware description language in a proof system: motivation and applications
Kees G. W. Goossens · 1993
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 2 which we use, its formal structural operational semantics, and its embedding in the higher-order logic proof system Lambda 3 . 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. Keyword Codes: B.7.2; F.3; I.2.3 Keywords: Integrated Circuits, Design Aids; Logics and Meaning of Programs; Deduction and Theorem Proving 1 Structure and Behaviour in Hardware Verification Hardware description languages (hdls) are a notation to describe designs of hardware. There is a wide spectrum of hdls [23]; examples are ddl [8], el...