Bryan Brady and Randal Bryant and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2008-136

October 20, 2008

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.pdf

Term-level verification is a formal technique that seeks to verify RTL hardware descriptions by abstracting away details of data representations and operations. The key to making term-level verification automatic and efficient is in deciding what to abstract. We investigate this question in this paper and propose a solution based on the use of type qualifiers. First, we demonstrate through case studies that only selective term-level abstraction can be very effective in reducing the run-time of formal tools while still retaining precision of analysis. Second, the term-level abstraction process can be guided using lightweight type qualifiers. We present an annotation language and type inference scheme that is applied to the formal verification of the Verilog implementation of a chip multiprocessor router. Experimental results indicate type-based selective term-level abstraction is effective at scaling up verification with minimal designer guidance.

---

BibTeX citation:

@techreport{Brady:EECS-2008-136,
    Author= {Brady, Bryan and Bryant, Randal and Seshia, Sanjit A.},
    Title= {Abstracting RTL Designs to the Term Level},
    Year= {2008},
    Month= {Oct},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html},
    Number= {UCB/EECS-2008-136},
    Abstract= {Term-level verification is a formal technique that seeks to verify RTL hardware descriptions by abstracting away details of data representations and operations. The key to making term-level verification automatic and efficient is in deciding what to abstract. We investigate this question in this paper and propose a solution based on the use of type qualifiers. First, we demonstrate through case studies that only selective term-level abstraction can be very effective in reducing the run-time of formal tools while still retaining precision of analysis. Second, the term-level abstraction process can be guided using lightweight type qualifiers. We present an annotation language and type inference scheme that is applied to the formal verification of the Verilog implementation of a chip multiprocessor router. Experimental results indicate type-based selective term-level abstraction is effective at scaling up verification with minimal designer guidance.},
}

EndNote citation:

%0 Report
%A Brady, Bryan 
%A Bryant, Randal 
%A Seshia, Sanjit A. 
%T Abstracting RTL Designs to the Term Level
%I EECS Department, University of California, Berkeley
%D 2008
%8 October 20
%@ UCB/EECS-2008-136
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html
%F Brady:EECS-2008-136