Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Abstracting RTL Designs to the Term Level

Bryan Brady, Randal Bryant and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2008-136
October 20, 2008

http://www.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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2008},
    Month = {Oct},
    URL = {http://www.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://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html
%F Brady:EECS-2008-136