Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


ucin1001432470.pdf (985.65 KB)

ETD Abstract Container

Abstract Header

FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS

TEICA, ELENA
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

Abstract Details

2001, PhD, University of Cincinnati, Engineering : Computer Science and Engineering.
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 properties, and the completeness property is a higher-order predicate that defines a complete set of functions. The specification and proof exercise are conducted in the Prototype Verification System (PVS). The use of PVS for the formal treatment presented in this thesis is justified not only by the typed higher-order logic that underlies its specification and proving environment (required by the very nature of the problem we are dealing with), but also by its rich language constructs that allow expressive and efficient specifications. As an alternative to an error prone axiomatic approach, each transformation is specified in a definitional manner. The correctness of each transformation is defined as the behavior preserving property: a transformation is correct if the extracted computational behavior of the output registers is the same in the initial and in the transformed design. Each transformation is mechanically proved correct in PVS based on the assumption that a set of preconditions is satisfied. A finite set of correct RTL transformations is said to be complete if and only if for any two RTL designs that implement the same behavior description, one design can be derived from the other by applying a finite sequence of transformations contained in this set. In other words, any possible implementation of a given behavior can be synthesized by applying only certain transformations to an initial implementation. We formalized and mechanically proved in PVS the completeness property using a constructive approach. The proof is constructive in the sense that a finite sequence of ransformations (belonging to the complete set), that transforms a certain design implementation into another one having the same behavior, is algorithmically defined. Some of the practical uses of the theoretical results formally established are: 1. A transformational derivation synthesis system based on the core set of RTL transformations presented here will yield correct-by-construction designs (if correctly implemented). The completeness property of this set ensures a virtually exhaustive search of the design space. 2. Any high-level synthesis algorithm that performs only structural optimizations can be viewed as a sequential application of RTL transformations. Having identified a complete finite set of transformations, then it can be asserted that any correct application of a synthesis algorithm should be assimilable with a sequence of transformations of the complete set. One can check the correctness of the synthesis process by attempting to identify such sequences.
Dr. Ranga Vemuri (Advisor)
191 p.
RTL Transformations; Formal Synthesis; Correctness Behavior Preserving Completeness; Mechanized in Higher-Order Logics of PVS

Recommended Citations

Citations

  • TEICA, E. (2001). FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS [Doctoral dissertation, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

    APA Style (7th edition)

  • TEICA, ELENA. FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS. 2001. University of Cincinnati, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470.

    MLA Style (8th edition)

  • TEICA, ELENA. "FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS." Doctoral dissertation, University of Cincinnati, 2001. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

    Chicago Manual of Style (17th edition)

ucin1001432470
694
© 2001, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.