# Hardware Model Checking Algorithms and Techniques
## 6 Ic3
If that is not the case, a counterexample of length zero, comprising only the initial state \(s\) violating the property, is found and the procedure outputs a failure. During each outer iteration (lines 6-17), the algorithm tries to prove that \(P\) is satisfied up to \(k\) steps in \(\mathcal{M}\), for increasing values of \(k\). Inner iterations of the algorithm refine the trace \(\mathbf{F_{k}}\) computed so far by adding new relative inductive clauses to some of its frames (lines 7-11). The algorithm iterates until either an inductive strengthening of the property is generated (line 16) or a counterexample to the property is found (line 11). ```
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}\}\) and \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample. 1:procedure\(\textsc{IC3}(\mathcal{M},P)\)
2:\(k\gets 0\)
3:\(F_{0}\leftarrow\mathcal{I}\)
4:if\(\exists s\models F_{0}\land\
eg P\)then
5:return\(\langle\textsc{Fail},(s)\rangle\)
6:repeat
7:while\(\exists s\models F_{k}\land\
eg P\)do
8:\(q\leftarrow\textsc{Extend}(s)\)
9:\(\langle\mathit{res},\mathit{cex}\rangle\leftarrow\textsc{BlockCube}(q,Q, \mathbf{F_{k}})\)
10:if\(\mathit{res}\)= Failthen
11:return\(\langle\textsc{Fail},\mathit{cex}\rangle\)
12:\(F_{k+1}\leftarrow\emptyset\)
13:\(k\gets k+1\)
14:Propagate(\(\mathbf{F_{k}}\))
15:if\(F_{i}=F_{i+1}\) for some \(0\leq i<k\)then
16:return\(\langle\textsc{Success},-\rangle\)
17:until forever
```  
**Algorithm 6** Top-level procedure of the IC3 algorithm: IC3 (\(\mathcal{M},P\)). At a given outer iteration \(k\), the algorithm has already computed a monotonic and safe trace. From Lemma 5, it follows that \(P\) is satisfied up to \(k-1\) steps in \(\mathcal{M}\). IC3 then tries to prove that \(P\) is satisfied up to \(k\) steps as well, by enumerating states of \(F_{k}\) that violate \(P\) and trying to block them in \(F_{k}\). **Definition 85** (Cube Blocking). : _Blocking a state (or, more generally, a cube) \(q\) in a frame \(F_{k}\) means to prove \(q\) unreachable within \(k\) steps in \(\mathcal{M}\) and, consequently, to refine \(F_{k}\) so that \(q\) is excluded from its overapproximation._  
To enumerate each state of \(F_{k}\) that violates \(P\) (line 7), the algorithm looks for states \(s\) in \(F_{k}\land\
eg P\). Such states are called _bad states_ and can be found as satisfying assignments for the following SAT query:  
\[\textsc{SAT}\?(F_{k}\land\
eg P) \tag{57}\]  
If a bad state \(s\) can be found (i.e., Query (57) is SAT), the algorithm tries to block it in \(F_{k}\). To increase performance of the algorithm, as suggested in [50], the bad state \(s\) found is first extended to a bad cube \(q\) by removing, if possible, some of its literals. Figure 7(a) visualizesthis step. The Extend(s) procedure (line 8), not reported here, performs this operation via either ternary simulations [50] or other SAT-based procedures [51]. The resulting cube \(q\) is stronger than \(s\) and it still violates \(P\); it is thus called a _bad cube_. The algorithm then tries to block the bad cube \(q\) in frame \(k\) rather than \(s\). It is shown in [50] that extending bad states into bad cubes before blocking them dramatically improves IC3 performance. The bad cube \(q\) is blocked in \(F_{k}\) calling the BlockCube(\(q\), \(Q\), \(F_{k}\)) procedure (line 9), described in Algorithm 7. When no further bad states can be found, the conditions in Definition 82 hold for \(k+1\) and IC3 can safely move to the next outer iteration, i.e., trying to prove that \(P\) is satisfied up to \(k+1\) steps. Before moving to the next iteration, a new empty frame \(F_{k+1}\) is created (line 12). Initially, \(\text{clauses}(F_{k+1})=\emptyset\), so that \(F_{k+1}=\top\). Note that \(\top\) is a valid overapproximation to the set of states reachable within \(k+1\) steps in \(\mathcal{M}\).