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.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 279-294 |
| Number of pages | 16 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 128 |
| Issue number | 6 |
| DOIs | |
| State | Published - May 23 2005 |
| Externally published | Yes |
| Event | Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004) - Duration: Sep 4 2004 → Sep 4 2004 |
Keywords
- Abstraction based Verification
- Conditioned Slicing
- Hardware Description Languages
- Hardware Verification
- LTL property
- Model Checking
- Program Slicing
- Safety properties
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)