# Hardware Model Checking Algorithms and Techniques
## 7 Igr
### Cone Unwinding and Rewinding
#### 7.3.2 Cone Rewinding
```
0:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\); \(\mathbf{F_{k}}\) a trace; \(i\) start step of the traversal; \(k\) bound of a backward unrolling from the target. 0:\(\langle\mathit{res},i_{hit},k_{hit}\rangle\) with \(\mathit{res}\in\{\textsc{Unreach},\textsc{Under}\}\); \(i_{hit}\) the step (if any) at which the cone is hit during traversal; \(k_{hit}\) the depth of the cone hit. 1:procedureIgrApproxForwardTraversal(\(\mathcal{M},P,\mathbf{F_{k}}\), \(k\))
2:\(R\leftarrow\mathsf{V}_{j=0}^{i}\,F_{j}\)
3:\(\mathit{rewind}\leftarrow\bot\)
4:\(i_{hit}\gets i\)
5:\(k_{hit}\gets k\)
6:while\(\top\)do
7:if\(i=|\mathbf{F_{k}}|\)then
8:\(\mathbf{F_{k}}[i+1]\leftarrow\top\)
9:if\(\mathit{rewind}\wedge k>0\)then
10:\(k\gets k-1\)
11:\(A\gets F_{i}(V^{0})\wedge T(V^{0},V^{1})\)
12:\(B\leftarrow\textsc{TraceSimplify}(Cone(1,k),\mathbf{F_{k}},i+1,k)\)
13:if\(\exists\pi^{0,k}\models A\wedge B\)then
14:\(\mathit{rewind}\leftarrow\top\)
15:\(i_{hit}\gets i\)
16:\(k_{hit}\gets k\)
17:else
18:\(I\leftarrow\textsc{Itp}(A,B)\)
19:\(F_{i+1}\leftarrow\textsc{Simplify}(F_{i+1},I)\wedge I\)
20:if\(\
ot\exists\mathsf{res}\models F_{i+1}\land\
eg\mathsf{R}\)then
21:return\(\langle\textsc{Unreach},-,-\rangle\)
22:\(R\gets R\lor F_{i+1}\)
23:\(i\gets i+1\)
24:if\(\
eg\mathit{rewind}\wedge i>D\)then
25:\(\mathit{rewind}\leftarrow\top\)
26:\(i_{hit}\gets i\)
27:\(k_{hit}\gets k\)
28:elseif\(\mathit{rewind}\wedge k=0\)then
29:return\(\langle\textsc{Undef},i_{hit},k_{hit}\rangle\)
```  
**Algorithm 13** Inner procedure that keeps track of the computed interpolants using a trace. At each iteration, the Unwind procedure described in Algorithm 14 computes \(i\) and \(k\), starting from \(i_{hit}\) and \(k_{hit}\), relative to the previous spurious counterexample. Following the strategy described in Section 7.3.1, the cone bound \(k\) is extended while \(i\) is decremented (lines 5-6), until either the algorithm encounters an Unsat BMC check or the initial states are reached (line 4). In the former case, Unwind managed to find a frame at which starting a traversal is expected to lead to a \(\mathbf{F_{k}}\) refinement and to filtering out the last spurious counterexample found. The procedure then returns an Undef result alongside the corresponding values for \(i\) and \(k\) (line 9). In the latter case, the procedure has detected an actual counterexample as a side effect. The procedure then returns a Reach result alongside the counterexample (line 8). ```
0:\(\mathcal{M}\stackrel{{\text{def}}}{{=}}\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\); \(i_{hit}\) the step at which the cone was hit during traversal; \(k_{hit}\) the depth of the cone hit. 0:\(\langle\mathit{res},\mathit{cex},i,k\rangle\) with \(\mathit{res}\in\{\textsc{Undef},\textsc{Reach}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample; \(i\) step at which resume forward traversal from; \(k\) cone depth to use in the resumed traversal. 1:procedureUnwind(\(\mathcal{M}\), \(P\), \(i_{hit}\), \(k_{hit}\))
2:\(i\gets i_{hit}\)
3:\(k\gets k_{hit}\)
4:while\(i\geq 0\land\exists\pi^{0,k}\models F_{i}(V^{0})\land T(V^{0},V^{1})\wedge Cone(1,k)\)do
5:\(i\gets i-1\)
6:\(k\gets k+1\)
7:if\(i<0\)then
8:return\(\langle\textsc{Reach},\pi^{0,k},-,-\rangle\)
9:return\(\langle\textsc{Undef},-,i,k\rangle\)
```  
**Algorithm 14** Unwinding procedure of IGR.