Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

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

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 2008-02, Vol.27 (2), p.366-379
Main Authors: Jain, H., Kroening, D., Sharygina, N., Clarke, E.M.
Format: Article
Language:English
Subjects:
Algorithms
Arithmetic
Boolean functions
Computation
Computer programs
Concrete
Concurrent computing
Data structures
Design engineering
Hardware
Hardware design languages
Laboratories
Logic
Mathematical models
Model checking (MC)
Position (location)
predicate abstraction
Program verification (computers)
refinement
Refining
register transfer level (RTL)
satisfiability (SAT)
State-space methods
Studies
verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0278-0070
1937-4151
DOI:10.1109/TCAD.2007.907270