SynGuide: An environment for doing interactive correctness preserving transformations

The authors present an overview of the meaning of Guided Synthesis by means of transformational design. They discuss the designer aspect of interaction with a specific Hardware Description Language to transform an original behavioral specification down to a level where an implementation can be done with logic synthesis tools or silicon compilers. A formal method for the optimization of a specification in a guaranteed correct way is presented. The method is based on the concept of improving a design by using a limited set of transformations that are proven to be correct. An environment enabling the user to do the transformations is created by using the Cornell Synthesizer Generator