A transformational approach to register-transfer-level design-space exploration
Ranga R. Vemuri · 1989
This thesis investigates the specification, correctness, and completeness issues of structural transformations used for register-transfer (RT) level hardware design-space exploration and synthesis. We develop a formal model of RT-level digital structures. The formalism has components to describe data paths, control graphs and control-step assignment to the control points in the presence of parallel, conditional and iterative control constructs. We define structural implementations of behaviors and equivalence of structures based a notion of syntactic comparison called value transfer preservation. We define the normal-form structure and show its uniqueness among a class of equivalent structures. We develop a set of elementary structural transformations. There are 18 transformations arranged into 6 groups. We prove the correctness of each transformation. Each elementary transformation has an inverse elementary transformation. We define and prove the completeness of the set of elementary transformations within our formal model. This is accomplished by constructing a terminating algorithm which transforms any structure in our model into an equivalent normal form structure by applying only the elementary transformations. We believe that our transformational model is realistic enough in expressive power to deal with a wide class of RT-level hardware design problems. We extract several 'optimizing' transformations from the existing literature on RT-level synthesis and show that these transformations can be expressed as a sequence of our transformations. We also bring out the limitations of our model and suggest possible extensions. Some of the transformations developed in the thesis are implemented, in Prolog, to aid us in assessing their use by experimentation.