*banner
 

Selective Term-Level Abstraction Using Type-Inference
Bryan Brady

Citation
Bryan Brady. "Selective Term-Level Abstraction Using Type-Inference". Talk or presentation, 13, March, 2007.

Abstract
Term-level verification is a formal technique that seeks to verify RTL hardware descriptons by abstracting away details of data representations and operations. The key to making term-level verification automatic and efficient is deciding what to abstract. Using abstraction in the wrong places will result in spurious counter examples; not using abstraction and precisely modeling RTL at the word-level, will result in large and inefficient verification models. Our initial results indicate that a combination of word-level reasoning with selective term-level abstraction can make verification more efficient. However, creating abstractions by hand is a time-consuming and error-prone process. We present a type-inference based algorithm that will semi-automatically generate abstractions from RTL models. This process avoids human-introduced errors and eliminates the need to manually create a separate verification model. To show that type-inference-based abstraction is useful, we plan on performing Burch and Dill style processor-verification on the OpenSPARC processor. As this is still a work in progress, the main goal of this presentation is to get early feedback.

Electronic downloads

Citation formats  
  • HTML
    Bryan Brady. <a
    href="http://chess.eecs.berkeley.edu/pubs/268.html"
    ><i>Selective Term-Level Abstraction Using
    Type-Inference</i></a>, Talk or presentation, 
    13, March, 2007.
  • Plain text
    Bryan Brady. "Selective Term-Level Abstraction Using
    Type-Inference". Talk or presentation,  13, March, 2007.
  • BibTeX
    @presentation{Brady07_SelectiveTermLevelAbstractionUsingTypeInference,
        author = {Bryan Brady},
        title = {Selective Term-Level Abstraction Using
                  Type-Inference},
        day = {13},
        month = {March},
        year = {2007},
        abstract = {Term-level verification is a formal technique that
                  seeks to verify RTL hardware descriptons by
                  abstracting away details of data representations
                  and operations. The key to making term-level
                  verification automatic and efficient is deciding
                  what to abstract. Using abstraction in the wrong
                  places will result in spurious counter examples;
                  not using abstraction and precisely modeling RTL
                  at the word-level, will result in large and
                  inefficient verification models. Our initial
                  results indicate that a combination of word-level
                  reasoning with selective term-level abstraction
                  can make verification more efficient. However,
                  creating abstractions by hand is a time-consuming
                  and error-prone process. We present a
                  type-inference based algorithm that will
                  semi-automatically generate abstractions from RTL
                  models. This process avoids human-introduced
                  errors and eliminates the need to manually create
                  a separate verification model. To show that
                  type-inference-based abstraction is useful, we
                  plan on performing Burch and Dill style
                  processor-verification on the OpenSPARC processor.
                  As this is still a work in progress, the main goal
                  of this presentation is to get early feedback.},
        URL = {http://chess.eecs.berkeley.edu/pubs/268.html}
    }
    

Posted by Christopher Brooks on 29 May 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

You are not logged in 
©2002-2014 Chess