Transformations in High Level Synthesis: Axiomatic Specification and Efficient Mechanical Verification

ID
TR-94-16
Authors
P. Sreeranga Rajan
Publishing date
May 1994
Length
71 pages
Abstract
In this work, we investigate the specification and mechanical verification of the correctness of transformations used during high level synthesis in hardware design. The high level synthesis system we address here is due, in part, to the SPRITE project at Philips Research Labs. The transformations in this system are used for refinement and optimization of descriptions specified in a signal flow graph language called SPRITE Input Language (SIL). SIL is an intermediate language used during the synthesis of hardware described using languages such as VHDL. Besides being an intermediate language, it also forms the backbone of TRADES synthesis system from University of Twente. SIL has been used in the design of hardware for audio and video applications. We use Prototype Verification System (PVS) from SRI International, to specify and verify the correctness of the transformations. The PVS specification language allows us to investigate the correctness problem using a convenient level of representation. While, the PVS verifier features automatic procedures and interactive verification rules to check properties of specifications. It has permitted us to examine not only the correctness, but also generalization and composition of transformations of SIL.