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

• DEStalk2007.ppt · application/vnd.ms-powerpoint · 1081 kbytes

• 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.