Efficient model checking of hardware using conditioned slicing

Shobha Vasudevan, E. Allen Emerson, Jacob A. Abraham

Research output: Contribution to journalConference articlepeer-review

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 languageEnglish (US)
Pages (from-to)279-294
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume128
Issue number6
DOIs
StatePublished - May 23 2005
Externally publishedYes
EventProceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004) -
Duration: Sep 4 2004Sep 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
  • General Computer Science

Fingerprint

Dive into the research topics of 'Efficient model checking of hardware using conditioned slicing'. Together they form a unique fingerprint.

Cite this