A REFINEMENT CALCULUS FOR THE SYNTHESIS OF VERIFIED HARDWARE DESCRIPTIONS IN VHDL

A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here . Refinement can be used to develop hardware description code that is ''correct by construction.'' The calculus is closely related to a Hoar e-style programming logic for VHDL and real-time systems in general. T hat logic and a semantics for a core subset of VHDL are described. The programming logic and the associated refinement calculus are shown to be complete. This means that if there is a code that can be shown to implement a. given specification, then it will be derivable from the s pecification via the calculus.