Dependency graphs are used to model data and control flow in hardware and software design. In high-level synthesis of hardware, optimization and refinement transformations are used to transform dependency-graph-based specifications at the behavior level to dependency-graph-based implementations at the register-transfer level. Register transfer-Ievel implementations are mapped to gate-level hardware designs by low-level logic synthesis. In this work, we investigated the specification and mechanical verification of the correctness of transformations used in high-level synthesis of hardware. We have provided a formal specification of dependency graphs, and verified the correctness of a variety of transformations used in an industrial synthesis framework. Errors have been discovered in the transformations, and modifications have been proposed and incorporated. Further, the formal specification has permitted us to examine the generalization and composition of transformations. In the process, we have discovered new transformations that could be used for further optimization and refinement than were possible before. The specification and verification schemes are general enough for applications in other synthesis frameworks and software design, where a transformational design approach is used. In order to present our work in a concrete context, we focus on the high-level synthesis part of the SPRITE project at Philips Research Laboratories. The transformation in the high-level synthesis system are used for refinement and optimization of descriptions specified in a dependency graph language called the SPRITE Input Language (SIL). SIL is an intermediate language used during the synthesis of hardware described using languages such as VHDL, SILAGE and ELLA. Besides being an intermediate language, it forms the backbone of the TRADES synthesis system of the University of Twente. SIL has been used in the design of hardware for audio and video applications. We used the Prototype Verification System (PVS) from SRI International to specify and mechanically verify the correctness of the transformations. The PVS specification language allows us to investigate the correctness problem using a eonveniellt level of representation. The PVS verifier features automatic procedures and interactive verification rules to cheek properties of specifications.

• csl-94-10.dvi
• csl-94-10.pdf
• csl-94-10.ps