# Hardware Model Checking Algorithms and Techniques
## 6 Ic3
After creating a new frame, a phase called _clause propagation_ takes place (line 14). During such a phase, IC3 tries to refine every frame \(F_{i}\), with \(0<i\leq k\), by checking whether some of its clauses can be pushed forward to the following frame. Possibly, clause propagation refines the outermost frame \(F_{k}\) so that an inductive invariant is reached. The propagation phase can lead to two adjacent frames becoming equivalent (see Figure 8g). If that happens, the algorithm has found an inductive strengthening of \(P\) for \(\mathcal{M}\) (equal to those frames). Therefore, following Lemma 6, property \(P\) holds for every reachable state of \(\mathcal{M}\) and IC3 returns a successful result (line 16). Procedure Propagate(\(F_{k}\)), described and discussed later, handles the clause propagation phase. The purpose of procedure BlockCube(\(q\), \(Q\), \(F_{k}\)) is to refine the trace \(F_{k}\) in order to block a bad cube \(q\) in \(F_{k}\). To preserve _image approximation_, prior to blocking a cube in a certain frame, IC3 has to recursively block predecessors of that cube in the preceding frames. To keep track of the states (or cubes) that must be blocked in certain frames, IC3 uses the formalism of _proof obligations_. **Definition 86** (Proof Obligation). : _Given a cube \(q\) and a frame \(F_{j}\), a proof obligation is a couple \((q,j)\) formalizing the fact that \(q\) must be blocked in \(F_{j}\)._  
Given a proof obligation \((q,j)\), the cube \(q\) can either represent a set of bad states or a set of states that can reach a bad state in some number of transitions. The index \(j\) indicates the position in the trace where \(q\) must be proved unreachable, or else the property fails. **Definition 87** (Discharging Proof Obligations). : _A proof obligation \((q,j)\) is said to be discharged when \(s\) becomes blocked in \(F_{j}\)._Figure 8: Visual representation of different steps in the IC3 procedure. In **(a)**, a bad cube \(s\) that violates \(P\) is found in \(F_{k}\) and extended to \(q\). **(b)** shows the beginning of the cube blocking procedure for \(q\), in which a clause \(\
eg q\) is checked for induction relative to \(F_{k-1}\). **(c)** shows the case in which relative induction of \(\
eg q\) does not hold and thus a predecessor cube \(s\) is found to be a CTI and extended into cube \(p\) that needs to be blocked in \(F_{k-1}\). **(d)** shows the cube blocking procedure for \(p\), in which a clause \(\
eg p\) is checked for induction relative to \(F_{k-2}\). In **(e)**, \(\
eg p\) is found to be inductive relative to \(F_{k-2}\); thus, \(\
eg p\) undergoes inductive generalization and the result is used to refine the trace. In **(f)**, after refining the trace, \(\
eg q\) becomes inductive relative to \(F_{k-1}\); the proof obligation of \(q\) can thus be discharged by generalizing \(\
eg q\) and refining the trace once more. In **(g)**, a fix-point is found by detecting \(F_{k}=F_{k+1}\) after propagation. In order to discharge a proof obligation, new ones may have to be recursively discharged. This can be carried out through a recursive implementation of the cube blocking procedure. However, in practice, handling proof obligations using a priority queue \(Q\) proved to be more efficient [50] and it is thus the commonly used approach in most state-of-the-art IC3 implementations. While blocking a cube, proof obligations \((q,j)\) are extracted from \(Q\) and discharged for increasing values of \(j\), ensuring that every predecessor of a bad cube \(q\) will be blocked in \(F_{j}\) (\(j<k\)) before \(q\) will be blocked in \(F_{k}\). In the BlockCube(\(q\), \(\mathcal{Q}\), \(\mathbf{F_{k}}\)) procedure, described in Algorithm 7, the queue of proof obligations is initialized with \((q,k)\), encoding the fact that \(q\) must be blocked in \(F_{k}\) (line 2). Then, proof obligations are iteratively extracted from the queue and discharged (lines 3-14). Prior to discharging a proof obligation \((q,j)\), IC3 checks whether that proof obligation still needs to be discharged.