Introduction

Abstract

Hardware Description Languages (HDLs) are used extensively to specify, verify, and document hardware designs. Typically, an HDL specification is compiled, elaborated, and then simulated. The hardware description language VHDL is one of the more widely supported language for specifying hardware designs. Academic and industrial researchers, along with CAD vendors have provided extensive tool support for VHDL. The official specification of the syntax and the semantics of VHDL is the Language Reference Manual (LRM) [27] which describes the language informally in English prose form. Unfortunately, it is impossible to formally validate simulation results or optimizations to the simulation process using this informal specification. Furthermore, a formal specification on paper is not of much use, since it is not possible to determine the accuracy of the results proven using the semantics. A formal semantics of the language must be developed and embedded in an automated theorem proving environment in order to validate optimizations.