# Hardware Model Checking Algorithms and Techniques
## 6 Ic3
The procedure computes a minimal inductive sub-clause, i.e., a sub-clause that is inductive relative to \(F_{j-1}\) and no further literals can be dropped without forgoing inductiveness [52]. In the general case, though, finding a minimal inductive sub-clause is often inefficient [48] and, thus, most implementations of IC3 rely on an approximate version of such a procedure. Approximate inductive generalization is significantly less expensive, yet still able to drop a reasonable number of literals. ```
1:\(j\) a frame index; \(q\) a cube such that \(F_{j-1}\wedge\
eg q\wedge T\rightarrow\
eg q^{\prime}\); \(\mathbf{F_{k}}\) the trace. 2:\(c\) a clause such that \(c\subseteq\
eg q\) and \(F_{j-1}\wedge c\wedge T\to c^{\prime}\). 3:procedureGeneralize(\(j\), \(q\), \(\mathbf{F_{k}}\))
4:\(c\leftarrow\
eg q\)
5:for all literals \(l\) in \(c\)do
6:\(t\gets c\setminus l\)
7:if\(\exists s,s^{\prime}\models F_{j-1}\wedge t\wedge T\wedge\
eg t^{\prime}\)then
8:if\(\exists s\models\mathcal{I}\wedge\
eg t\)then
9:\(c\gets t\)
10:return\(c\)
```  
**Algorithm 8** Iterative inductive generalization procedure: Generalize (\(j\), \(s\), \(\mathbf{F_{k}}\))  
In the \(\textsc{Generalize}(j,q,\mathbf{F_{k}})\) procedure, a clause \(c\) initialized with \(\
eg q\) (line 2) represents the current inductive sub-clause. For each literal of \(c\), the candidate clause \(t\) is obtained by discarding that literal from \(c\) (line 4). Dropping literals from a relative inductive clause can violate both initiation and relative consecution conditions of induction. The candidate clause \(t\) must thus be checked for inductiveness relative to \(F_{j-1}\). IC3 checks whether the relative consecution condition (\(F_{j-1}\wedge t\wedge T\to t^{\prime}\)) keeps holding for \(t\) by posing the following SAT query:  
\[SAT?(F_{j-1}\wedge t\wedge T\wedge\
eg t^{\prime}) \tag{60}\]  
If the relative consecution condition holds (i.e, Query (60) is UNSAT), the algorithm needs to prove the initiation condition of induction (\(\mathcal{I}\to t\)). This check (line 6) can be performed either syntactically or semantically. If \(\mathcal{I}\) can be described as a cube, it is enough to check whether at least one of the literals of \(\mathcal{I}\) appears in \(t\) with opposite polarity. In such a case, \(\
eg t\) does not intersect \(\mathcal{I}\) and the initiation condition holds. Otherwise, the initiation of induction must be checked explicitly by posing the following SAT query:  
\[SAT?(\mathcal{I}\land\
eg t) \tag{61}\]  
If Query (61) is UNSAT, the initiation condition holds for \(t\). If both the relative consecution and the initiation conditions still hold for the candidate clause \(t\), the current inductive sub-clause \(c\) can be updated with \(t\) (line 7). The Propagate (\(\mathbf{F_{k}}\)) procedure (Algorithm 9) manages the propagation phase. For every clause \(c\) of each frame \(F_{j}\), with \(0\leq j<k-1\), it checks whether \(c\) can be pushed forward to \(F_{j+1}\). This is performed by checking whether \(c\) is inductive relative to \(F_{j}\) (line 4). The procedure must check whether relative consecution \(F_{j}\land c\land T\to c^{\prime}\) holds, by answering the following SAT query:  
\[SAT?(F_{j}\land c\land T\land\
eg c^{\prime}) \tag{62}\]  
If relative consecution holds (i.e., Query (62) is UNSAT), then \(c\) is relative inductive to \(F_{j}\) and can be pushed forward to \(F_{i+1}\). Otherwise, \(c\) cannot be pushed forward and the algorithm moves to the next iteration. ```
1:\(\mathbf{F_{k}}\): the current trace. 2:procedurePropagate(\(\mathbf{F_{k}}\))
3:for\(j=0\) to \(k-1\)do
4:for all\(c\in F_{j}\)do
5:if\(\exists s,s^{\prime}\models F_{j}\land c\land T\land\
eg c^{\prime}\)then
6:\(F_{j}\gets F_{j}\setminus\{c\}\)
7:\(F_{j+1}\gets F_{j+1}\cup\{c\}\)
```  
**Algorithm 9** Clause propagation procedure: Propagate (\(\mathbf{F_{k}}\)). Property Directed Reachability (PDR) is a variant implementation of IC3 proposed by [PERSON] et al. in [50].