A refinement calculus for VHDL

A refinement calculus for the specification of real-time systems and their refinement to a VHDL behavioural description is set out here. The specification format is a logical triple with the look of a Z or VDM schema. Choices from a short menu of refinement operations gradually convert an initial specification to VHDL code through a series of mixed mode intermediates. The calculus is complete in the sense that if there is a code of the VHDL subset considered here (unit-delay waits and signal assignments but no delta delays) satisfying the specification, then it can be obtained by applying some sequence of the refinement operations. The result is “correct by construction”