TexasScholarWorks
    • Login
    • Submit
    View Item 
    •   Repository Home
    • UT Electronic Theses and Dissertations
    • UT Electronic Theses and Dissertations
    • View Item
    • Repository Home
    • UT Electronic Theses and Dissertations
    • UT Electronic Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Combining advanced formal hardware verification techniques

    Thumbnail
    View/Open
    reebere64715.pdf (883.0Kb)
    Date
    2007-12
    Author
    Reeber, Erik Henry, 1978-
    Share
     Facebook
     Twitter
     LinkedIn
    Metadata
    Show full item record
    Abstract
    This dissertation combines formal verification techniques in an attempt to reduce the human effort required to verify large systems formally. One method to reduce the human effort required by formal verification is to modify general-purpose theorem proving techniques to increase the number of lemma instances considered automatically. Such a modification to the forward chaining proof technique within the ACL2 theorem prover is described. This dissertation identifies a decidable subclass of the ACL2 logic, the Subclass of Unrollable List Formulas in ACL2 (SUFLA). SUFLA is shown to be decidable, i.e., there exists an algorithm that decides whether any SUFLA formula is valid. Theorems from first-order logic can be proven through a methodology that combines interactive theorem proving with a fully-automated solver for SUFLA formulas. This methodology has been applied to the verification of components of the TRIPS processor, a prototype processor designed and fabricated by the University of Texas and IBM. Also, a fully-automated procedure for the Satisfiability Modulo Theory (SMT) of bit vectors is implemented by combining a solver for SUFLA formulas with the ACL2 theorem prover's general-purpose rewriting proof technique. A new methodology for combining theorem proving and model checking is presented, which uses a unique "black-box" formalization of hardware designs. This methodology has been used to combine the ACL2 theorem prover with IBM's SixthSense model checker and applied to the verification of a high-performance industrial multiplier design. A general-purpose mechanism has been created for adding external tools to a general-purpose theorem prover. This mechanism, implemented in the ACL2 theorem prover, is capable of supporting the combination of ACL2 with both SixthSense and the SAT-based SUFLA solver. A new hardware description language, DE2, is described. DE2 has a number of unique features geared towards simplifying formal verification, including a relatively simple formal semantics, support for the description of circuit generators, and support for embedding non-functional constructs within a hardware design. The composition of these techniques extend our knowledge of the languages and logics needed for formal verification and should reduce the human effort required to verify large hardware circuit models.
    Department
    Computer Sciences
    URI
    http://hdl.handle.net/2152/3662
    Collections
    • UT Electronic Theses and Dissertations

    University of Texas at Austin Libraries
    • facebook
    • twitter
    • instagram
    • youtube
    • CONTACT US
    • MAPS & DIRECTIONS
    • JOB OPPORTUNITIES
    • UT Austin Home
    • Emergency Information
    • Site Policies
    • Web Accessibility Policy
    • Web Privacy Policy
    • Adobe Reader
    Subscribe to our NewsletterGive to the Libraries

    © The University of Texas at Austin

     

     

    Browse

    Entire RepositoryCommunities & CollectionsDate IssuedAuthorsTitlesSubjectsDepartmentsThis CollectionDate IssuedAuthorsTitlesSubjectsDepartments

    My Account

    Login

    Statistics

    View Usage Statistics

    Information

    About Contact Policies Getting Started Glossary Help FAQs

    University of Texas at Austin Libraries
    • facebook
    • twitter
    • instagram
    • youtube
    • CONTACT US
    • MAPS & DIRECTIONS
    • JOB OPPORTUNITIES
    • UT Austin Home
    • Emergency Information
    • Site Policies
    • Web Accessibility Policy
    • Web Privacy Policy
    • Adobe Reader
    Subscribe to our NewsletterGive to the Libraries

    © The University of Texas at Austin