Number SRI-CSL-94-10.
Computer Science Laboratory, SRI International.
1994.
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-level
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 transformations 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 convenient level of representation. The PVS
verifier features automatic procedures and interactive verification rules to check properties of
specifications.
@techreport{sri-csl-94-10,
AUTHOR = {{P.} Sreeranga Rajan},
TITLE = {Transformations in High-Level Synthesis: Formal Specification and Efficient Mechanical Verification},
INSTITUTION = {Computer Science Laboratory, {SRI} International},
YEAR = {1994},
NUMBER = {{SRI-CSL-94-10}},
URL = {http://www.csl.sri.com/papers/sri-csl-94-10/}
}