Embedding a CHDDL in a proof system

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)


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 ...
Original languageEnglish
Title of host publicationAdvanced Research Workshop on Correct Hardware Design Methodologies
EditorsP. Prinetto, P. Camurati
PublisherNorth-Holland Publishing Company
Publication statusPublished - 1991


Dive into the research topics of 'Embedding a CHDDL in a proof system'. Together they form a unique fingerprint.

Cite this