# Using Cubes of Non-state Variables With Property Directed Reachability

## J. Backes, M. Riedel

### Proceedings of Design Automation and Test in Europe, Grenoble, France. 2013

A new SAT-Based algorithm for symbolic model
checking has been gaining popularity. This algorithm, referred
to as “Incremental Construction of Inductive Clauses for Indu-
bitable 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.