Embedding a CHDDL in a proof system

This paper describes how a formal semantics for a computer hardware design and description language may be embedded in a proof system. An abstraction of ELLA 1 , its formal structured operational semantics and the underlying semantic model are introduced. The Lambda 2 proof system, the embedding of the semantics and some results are discussed. Some examples are shown, and other approaches are briefly surveyed. 1 Introduction As circuits are getting larger and more complex, circuit design is becoming more difficult. The need to describe and document designs has led to the development of computer hardware design and description languages (CHDDLs) such as ELLA [Com90] and VHDL [Ins88]. Using these languages, a circuit may be described at all stages of its design, from the high level specification down to the gate level description. Traditionally simulators have been used to test designs at various levels. It is now impossible to fully test a design by simulation alone. Circuits are ...