Sciweavers

DAC
2005
ACM

Word level predicate abstraction and refinement for verifying RTL verilog

14 years 11 months ago
Word level predicate abstraction and refinement for verifying RTL verilog
el Predicate Abstraction and Refinement for Verifying RTL Verilog Himanshu Jain CMU SCS, Pittsburgh, PA 15213 Daniel Kroening ETH Z?urich, Switzerland Natasha Sharygina CMU SCS and SEI, Pittsburgh, PA 15213 Edmund Clarke CMU SCS, Pittsburgh, PA 15213 Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique ss this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. The llenge when using predicate abstraction is the discovery of suitable predicates. We propose to use weakest preconditions of Verilog statements in order to obtain ne...
Himanshu Jain, Daniel Kroening, Natasha Sharygina,
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2005
Where DAC
Authors Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Comments (0)