Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329461 | Electronic Notes in Theoretical Computer Science | 2005 | 16 Pages |
Abstract
In this work, we present an abstraction based property verification technique for hardware using conditioned slicing. We handle safety property specifications of the form G(antecedentâconsequent). We use the antecedent of the properties to create our abstractions, Antecedent Conditioned Slices. We extend conditioned slicing to Hardware Description Languages (HDLs). We provide a theoretical foundation for our conditioned slicing based verification technique. We also present experimental results on the Verilog RTL implementation of the USB 2.0. We demonstrate very high performance gains achieved by our technique when compared to static program slicing, using state-of-the-art model checkers.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Shobha Vasudevan, E. Allen Emerson, Jacob A. Abraham,