# Hardware Model Checking Algorithms and Techniques
## 7 Igr
### Cone Unwinding and Rewinding
#### 7.3.2 Cone Rewinding
The two sub-tasks are performed by Unwind and IGRApproxForwardTraversal, respectively. ```
0:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\). 0:\(\langle\mathit{res},\mathit{cex}\rangle\) with \(\mathit{res}\in\{\textsc{Success},\textsc{Fail}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample. 1:procedureIGRModelChecking(\(\mathcal{M}\), \(P\))
2:if\(\exists s_{0}:s_{0}\models\mathcal{I}(V)\land\
eg P(V)\)then
3:return\(\langle\textsc{Fail},(s_{0})\rangle\)
4:\(\mathbf{F_{k}}[0]\leftarrow\mathcal{I}\)
5:\(i_{hit}\gets 0\)
6:\(k_{hit}\gets 1\)
7:while true do
8:\(\langle\mathit{res},\mathit{cex},i,k\rangle\leftarrow\textsc{Unwind}(\mathcal{ M},P,\mathbf{F_{k}},i_{hit},k_{hit})\)
9:ifres is Reach then
10:return\(\langle\textsc{Fail},\mathit{cex}\rangle\)
11:\(\langle\mathit{res},i_{hit},k_{hit}\rangle\leftarrow\textsc{IGRApproxForwardTraversal}( \mathcal{M},P,\mathbf{F_{k}},i,k)\)
12:ifres is Unreach then
13:return\(\langle\textsc{Success},-\rangle\)
```  
**Algorithm 12** Top-level procedure of IGR. Procedure IGRApproxForwardTraversal, described in Algorithm 13, performs an overapproximated forward traversal of reachable states. The procedure starts from a given frame in the trace while preserving safety with respect to a cone of a given depth. It first computes the current overapproximated set of reachable states at step \(i\) by disjoining the first \(i\) frames (line 2). During each iteration of the traversal loop (lines 6-29), the algorithm then proceeds in two different ways taking into account whether or not _cone rewinding_ (see Section 7.3.2) has been triggered. If it has not been triggered, the algorithm performs a traversal step using a cone of bound \(k\). Conversely, the procedure decreases the bound of the cone at each iteration to perform rewinding (lines 9-10). The procedure then performs cone simplification (line 12), as described in Section 7.2, and checks whether the current set of overapproximated reachable states \(R\) hits the cone (line 13), during each traversal step. In case of a hit, the algorithm saves the current step and cone bound in \(i_{hit}\) and \(k_{hit}\), respectively, and triggers a refinement sequence (lines 14-16). Conversely, a new overapproximated image is computed through interpolation (lines 18) and the current frame \(F_{i}\) is refined and simplified (line 19) as described in Section 7.2. The algorithm then checks whether the overapproximation is an inductive invariant, returning Unreach if that is the case (lines 20-21). If no inductive invariant has been found, the new set of overapproximated forward reachable states to be used for the next iteration is computed as \(R\lor F_{i+1}\) (line 22). Each time the forward traversal reaches the end of the current trace, a new frame \(F_{i+1}\) is instantiated equal to \(\top\) and added to the trace (lines 7-8). At the end of each iteration, if a given depth threshold \(D\) has been reached, the algorithm forces rewinding (line 24-27). When rewinding is triggered, either after finding a spurious counterexample or by force, the algorithm continues the traversal decreasing the cone bound at each iteration. When the cone has been completely rewound, the algorithm terminates returning Under alongside the step and cone bound at which either a spurious counterexample was found (lines 15-16) or rewinding has been forced (lines 26-27). The aforementioned \(D\) threshold heuristically controls activation of cone rewinding. Whenever \(D=0\), rewinding is always active, so the approach obtains a minimal refinement while mimicking the effect of interpolation sequences [55]. High values of \(D\) keep the value constant until a hit, mimicking a scheme which would result far closer to standard interpolation. Empirically, it occurs that small values tend to be usually better at small sequential depths, as they can enact more, relatively inexpensive, refinement steps.