Design Verification and Transformation of Hardware Specifications to VHDL

Our innovative proposal is to apply the design refinement approach, as implemented in the Reacto Verification System (RVS), to construct verified VHDL models. RVS includes a specification language, with features fundamental to the specification of hardware systems, a graphical interface used to construct specifications; a verification subsystem that includes a verification condition generator, and a state-of-the-art theorem prover integrated into a comprehensive verification environment; a simulator used to rapid prototype a specification; and a transformation system used to transform specifications into target code using transformations formally proved to be correctness preserving. We propose to perform design studies to define extensions to Reacto for the specification and generation of VHDL hardware descriptions. These extensions include the construction a VHDL back-end to the transformation system, and extensions to the specification language, simulation environment, and verification environment. The design study will analyze one significant sample problem: a hardware implementation of the Data Encryption Standard (DES) algorithm. RVS leverages off of and contributes to the considerable technology base available at Kestrel. This project will be done in cooperation with Capt. Paul Bailor of AFIT.