Back to Search
Start Over
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
- Source :
-
IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems . Feb2008, Vol. 27 Issue 2, p366-379. 13p. 4 Black and White Photographs, 3 Charts, 10 Graphs. - Publication Year :
- 2008
-
Abstract
- As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RTL of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. This paper uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) the computation of the abstract model in presence of a large number of predicates and 2) the discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing the weakest preconditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We compare the performance of our technique with localization reduction, a netlist-level abstraction technique, and report improvements on a set of benchmarks. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 02780070
- Volume :
- 27
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems
- Publication Type :
- Academic Journal
- Accession number :
- 32929616
- Full Text :
- https://doi.org/10.1109/TCAD.2007.907270