Abstracting RTL Designs to the Term Level
Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, Bryan A. Brady, Randal E. Bryant · 2008
Term-level verication is a formal technique that seeks to verify RTL hardware descriptions by ab-stracting away details of data representations and operations. The key to making term-level verication automatic and efcient is in deciding what to abstract. We investigate this question in this paper and propose a solution based on the use of type qualiers. 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 qualiers. We present an annotation language and type inference scheme that is applied to the formal verication of the Verilog implementation of a chip multiprocessor router. Experimen-tal results indicate type-based selective term-level abstraction is effective at scaling up verication with minimal designer guidance. 1