Improved verification of hardware designs through antecedent conditioned slicing

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

Research output: Contribution to journalArticlepeer-review

Abstract

Static slicing has shown itself to be a valuable tool, facilitating the verification of hardware designs. In this paper, we present a sharpened notion, antecedent conditioned slicing that provides a more effective abstraction for reducing the size of the state space. In antecedent conditioned slicing, extra information from the antecedent is used to permit greater pruning of the state space. In a previous version of this paper, we applied antecedent conditioned slicing to safety properties of the form G (antecedent ⇒ consequent) where antecedent and consequent were written in propositional logic. In this paper, we use antecedent conditioned slicing to handle safety and bounded liveness property specifications written in linear time temporal logic. We present a theoretical justification of our technique. We provide experimental results on a Verilog RTL implementation of the USB 2.0 functional core, which is a large design with about 1,100 state elements (10331 states). The results demonstrate that the technique provides significant performance benefits over static program slicing using state-of-the-art model checkers.

Original languageEnglish (US)
Pages (from-to)89-101
Number of pages13
JournalInternational Journal on Software Tools for Technology Transfer
Volume9
Issue number1
DOIs
StatePublished - Feb 1 2007
Externally publishedYes

Keywords

  • Antecedent conditioned slicing
  • Hardware description languages
  • Hardware verification
  • LTL property
  • Model checking
  • Program slicing
  • Verilog RTL

ASJC Scopus subject areas

  • Software
  • Information Systems

Fingerprint Dive into the research topics of 'Improved verification of hardware designs through antecedent conditioned slicing'. Together they form a unique fingerprint.

Cite this