Formal correctness and completeness for a set of uninterpreted rtl transformations
Elena Teica, Ranga R. Vemuri · OhioLink ETD Center (Ohio Library and Information Network) · 2001
The work presented in this thesis is concerned with the correctness of the high-level synthesis process.In particular, it addresses transformational derivation (TD) systems.TD denominates a class of synthesis techniques wherein a register transfer level (RTL) implementation is derived by applying a sequence of behavior-preserving transformations to an initial behavior representation.We present in this thesis a formal treatment of correctness and completeness for a set of ten uninterpreted register transfer level transformations on which a TD system can be based.The formal definitions for RTL transformations are based on an uninterpreted model for RTL designs corresponding to straight-line code behavior descriptions.Our model specifies an abstract RTL design as a set of properties asserted about abstract collections (sets) of components (operators and registers).RTL transformations are functions operating on elements of the set defined by these To my thesis advisor, Dr. Ranga Vemuri, for the constant support and guidance, for letting me be one of the many young researchers he is fostering in the excellent working environment the DDEL lab is.