Using cubes of non-state variables with property directed reachability

John D. Backes, Marc Riedel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

A new SAT-Based algorithm for symbolic model checking has been gaining popularity. This algorithm, referred to as "Incremental Construction of Inductive Clauses for Indubitable Correctness" (IC3) or "Property Directed Reachability" (PDR), uses information learned from SAT instances of isolated time frames to either prove that an invariant exists, or provide a counter example. The information learned between each time frame is recorded in the form of cubes of the state variables. In this work, we study the effect of extending PDR to use cubes of intermediate variables representing the logic gates in the transition relation. We demonstrate that we can improve the runtime for satisfiable benchmarks by up to 3.2X, with an average speedup of 1.23X. Our approach also provides a speedup of up to 3.84X for unsatisfiable benchmarks.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE 2013
Pages807-810
Number of pages4
StatePublished - Oct 21 2013
Event16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013 - Grenoble, France
Duration: Mar 18 2013Mar 22 2013

Other

Other16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013
Country/TerritoryFrance
CityGrenoble
Period3/18/133/22/13

Fingerprint

Dive into the research topics of 'Using cubes of non-state variables with property directed reachability'. Together they form a unique fingerprint.

Cite this