Skip to Main Content
Frequently Asked Questions
Submit an ETD
Global Search Box
Need Help?
Keyword Search
Participating Institutions
Advanced Search
School Logo
Files
File List
ucin982064542.pdf (1.7 MB)
ETD Abstract Container
Abstract Header
AUTOMATED CORRECTNESS CONDITION GENERATION FOR FORMAL VERIFICATION OF SYNTHESIZED RTL DESIGNS
Author Info
MANSOURI, NAZANIN
Permalink:
http://rave.ohiolink.edu/etdc/view?acc_num=ucin982064542
Abstract Details
Year and Degree
2001, PhD, University of Cincinnati, Engineering : Computer Engineering.
Abstract
This work presents a formal methodology for verifying the functional correctness of synthesized register transfer level designs (RTL) generated by a high-level synthesis system. The verification is conducted by proving the observation equivalence of the RTL design with a description of its desired behavior. High-level synthesis tools generate register transfer level designs from algorithmic behavioral specifications. The high-level synthesis process consists of dependency graph scheduling,function unit allocation, register allocation, interconnect allocation and controller generation tasks. Widely used algorithms for these tasks retain the overall control flow structure of the behavioral specification allowing code motion only within basic blocks. Further, high-level synthesis algorithms are in general oblivious to the mathematical properties of arithmetic and logic operators, selecting and sharing RTL library modules solely based on matching uninterpreted function symbols and constants. Many researchers have noted that these features of high-level synthesis algorithms can be exploited to develop efficient verification strategies for synthesized designs. This dissertation reports a verification methodology that effectively exploits these features to achieve efficient and fully automated verification of synthesized designs. Contributions of this research include formalization and formulation in higher-order logic in a theorem proving environment mathematical models for the synthesized register transfer level designs and their behavioral specifications and a set of sufficient correctness conditions for these designs. It presents an in depth study of pipelining in design synthesis, and identifies the complete set of correctness conditions for RTL designs generated through the synthesis processes that employ pipelining techniques. This method has been implemented in a verification tool (the correctness condition generator, CCG) and is integrated with a high-level synthesis system. CCG generates (1) formal specifications of the behavior and the RTL design including the data path and the controller, (2) the correctness lemmas establishing equivalence between the synthesized RTL design and its behavioral specification, and (3) their proof scripts that can be submitted to a higher-order logic proof checker. The tool performs model extraction, correctness condition generation and proof generation automatically and without human interaction. This approach is based on the identification, by the synthesis tool during the synthesis process, of the binding between critical specification variables and criticalregisters in the RTL design and between the critical states in the behavior and the corresponding states in the RTL design. CCG is capable of handling a broad range of behavior constructs that may be used for specifying the behavior and a wide variety of algorithms that may be employed during the synthesis process. Also, the verification algorithms of CCG have the appealing feature of relying on symbolic analysis of the uninterpreted values of the variables and registers. This has resulted in a considerable reduction in verification time compared to other post-synthesis verification systems, that are often restrained by this factor,
Committee
Dr. Ranga Vemuri (Advisor)
Pages
301 p.
Keywords
formal verification
;
register transfer level (RTL)
;
High-level synthesis
;
correctness conditions
Recommended Citations
Refworks
EndNote
RIS
Mendeley
Citations
MANSOURI, N. (2001).
AUTOMATED CORRECTNESS CONDITION GENERATION FOR FORMAL VERIFICATION OF SYNTHESIZED RTL DESIGNS
[Doctoral dissertation, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin982064542
APA Style (7th edition)
MANSOURI, NAZANIN.
AUTOMATED CORRECTNESS CONDITION GENERATION FOR FORMAL VERIFICATION OF SYNTHESIZED RTL DESIGNS.
2001. University of Cincinnati, Doctoral dissertation.
OhioLINK Electronic Theses and Dissertations Center
, http://rave.ohiolink.edu/etdc/view?acc_num=ucin982064542.
MLA Style (8th edition)
MANSOURI, NAZANIN. "AUTOMATED CORRECTNESS CONDITION GENERATION FOR FORMAL VERIFICATION OF SYNTHESIZED RTL DESIGNS." Doctoral dissertation, University of Cincinnati, 2001. http://rave.ohiolink.edu/etdc/view?acc_num=ucin982064542
Chicago Manual of Style (17th edition)
Abstract Footer
Document number:
ucin982064542
Download Count:
1,068
Copyright Info
© 2001, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.