# Hardware Model Checking Algorithms and Techniques
## 7 Igr
### Cone Unwinding and Rewinding
#### 7.3.2 Cone Rewinding  
When, at a given step \(i\), the forward traversal hits the cone of depth \(k\), rather than starting a new traversal with an unwound cone, the algorithm can optionally continue the current traversal with a sequence of iterations, called _refinement sequence_. During refinement, each iteration uses a cone of decreasing depth for which the safety of the current reachable state overapproximation is guaranteed. Assume that, at a given step \(i\), \(F_{i}(V^{0})\wedge T(V^{0},V^{1})\wedge Cone(1,k)\) is Sat. Since \(F_{i}\) was proved to be safe with respect to \(Cone(1,k)\) at iteration \(i-1\), there does not exist any counterexample of length at most \(k\) starting from \(i\), and hence it is guaranteed that  
\[F_{i+j}(V^{0})\wedge T(V^{0},V^{1})\wedge Cone(1,k-j-1) \tag{67}\]  
is Unsat for each \(0\leq j<k-1\). A new interpolant \(I_{j}\) can be generated from each of such calls to be used to refine \(F_{i+j+1}\). Alternatively, one could compute an interpolation sequence directly from the BMC call (67) and use it to refine the trace. To summarize, once a cone of depth \(k\) is hit at step \(i\) of the forward traversal, the algorithm can compute a sequence of \(k\) interpolants, each representing an overapproximation of states reachable in \(i+j+1\) transitions, with \(0\leq j<k-1\), that can be used to refine, or generate, the frames \((F_{i+1},\ldots,F_{i+k})\) of the trace. The main purpose of such a refinement sequence is to let future traversals operate over more precise overapproximations of the reachable states. On such premises, the overall IGR algorithm can now be presented. The top-level procedure of IGR is reported in Algorithm 12. The algorithm first checks the safety of the initial states (lines 2-3) and initializes the trace \(\mathbf{F_{k}}\) (line 4). Indexes \(i_{hit}\) and \(k_{hit}\) are also initialized (line 5-6) and they are used to keep track of the traversal step and cone depth at which a cone was hit during the previous traversal, if any. Past initialization, the outer loop starts iterating overapproximated forward traversals (lines 7-13). Procedure Unwind is invoked first to seek the best frame at which to start the next traversal (line 8), to perform cone unwinding (as described in Section 7.3.1) starting from the step \(i_{hit}\) and cone depth \(k_{hit}\), until either a concrete counterexample or a frame that could be refined by computing a new interpolant is found. In the first case, Unwind returns a Reach result and a counterexample. The algorithm, thus, terminates with Fail producing the counterexample as output (lines 9-10). In the second case, Unwind returns an Under result, a step \(i\) and a cone depth \(k\) to be used for the next traversal. Note that, during the first iteration, \(i_{hit}\) and \(k_{hit}\) are initialized to zero and one, respectively; therefore, Unwind simply checks whether the initial states can reach the target in one transition. If no concrete counterexample is found, the algorithm starts a new forward overapproximated traversal by calling the IgrApproxForwardTraversal routine (line 11). Upon termination of such a procedure, if the result is Unreach then an inductive invariant has been found during traversal and thus the algorithm terminates with Success (lines 12-13). Conversely, the cone was hit and the traversal procedure returns an Undef result together with the step \(i_{hit}\) and cone depth \(k_{hit}\) at which that occurred. In such a scenario, it means that a spurious counterexample was found during traversal and the algorithm then iterates to perform a new traversal. On these premises, we can summarize the overall scheme of IgrModelChecking as follows:* Iteratively choose a starting frame \(F_{i}\) and a cone \(Cone(1,k)\) to be unwound with guidance throughout the overapproximated trace \(\mathbf{F_{k}}\). * Initiate a forward traversal from \(F_{i}\) with \(Cone(1,k)\) aiming at refining \(\mathbf{F_{k}}\) and filtering out the latest spurious counterexample found within \(F_{i_{hit}}\).