# Hardware Model Checking Algorithms and Techniques
## 7 Igr
### Frames and Cone Simplification  
In order to keep cones and overapproximations of reachable states contained in size, the algorithms exploit an optimization that aims at simplifying the representation of frames and/or bad cones through ad hoc redundancy removal, exploiting the general notion of redundancy removal under _observability don't cares_. In order to understand the approach, let us denote _simplification under a care set_ as the function \(\textsc{Simplify}(F,C)\), where \(F\) is a formula over \(V\) to be simplified and \(C\) is another formula over \(V\) to be used as a care set for the simplification of \(F\). The care set is defined with respect to a reference formula \(G\) over \(V\cup W\) in which \(F\) appears as a subformula, as follows. **Definition 88** (Care Set and Don't Care Set). : _Given a propositional formula \(F\) over \(V\) and another formula \(G\) over \(V\cup W\) such that \(F\) is a subformula of \(G\), we define the care set \(\operatorname{C}_{F}^{G}\) of \(F\) with respect to \(G\) as the set of assignments over \(V\) under which the value of \(F\) affects the value of \(G\). A care set for \(F\) with respect to \(G\) can be represented by the formula:_  
\[C_{F}^{G}=G\oplus G[F\leftarrow\
eg F] \tag{63}\]  
_The complement of \(C_{F}^{G}\) is called the don't care set of \(F\) with respect to \(G\). It represents the set of assignments over \(V\) under which the value of \(F\) does not affect the value of \(G\)._  
Simplification of a formula \(F\) under care set \(\operatorname{C}_{F}^{G}\) with respect to a reference formula \(G\) can entail the application of any number of equivalence-preserving or strengthening transformations over \(F\), as long as the following constraint is preserved:  
\[G\equiv G[F\leftarrow\textsc{Simplify}(F,\operatorname{C}_{F}^{G})] \tag{64}\]  
Computation of care sets and don't care sets can be costly [54]. Considering a conjunction \(F=A\wedge B\) as a reference formula, the following lemma describes two straightforward ways to obtain care sets for either one of the conjoined formulas. We focus on \(B\), since the same dual reasoning applies to \(A\). **Lemma 8** (Care Sets for Conjunctive Reference Formulas). : _Given \(A\) and \(B\), two propositional formulas over \(V\), and given \(F=A\wedge B\), then \(A\) is a care set for \(B\) with respect to \(F\). Given \(C\), a propositional formula over \(V\), such that \(A\to C\), then \(C\) is a care set for \(B\) with respect to \(F\)._  
Figure 9a,b illustrate the simplification of a formula \(B\) with respect to a reference formula \(F=A\wedge B\) under care sets as defined by Lemma 8, in terms of sets of assignments. Given two propositional formulas \(A=a\) and \(B=(a\lor b)\), the knowledge that any assignment satisfying their conjunction \(F=A\wedge B\) must be a satisfying assignment of either one can be used to simplify the other. Using \(A\) as a care set for \(B\), since \(F=a\wedge(a\lor b)\) is satisfied only by assignments satisfying \(A\) (i.e., assignments \(\mu\) such that \(\mu(a)=\top\)) it is possible to simplify \(B\) through the injection of a constant \(\top\) prior to conjoining it to \(A\), obtaining \(\top\lor b\equiv b\). The resulting formula after simplification \(A\wedge\textsc{Simplify}(B,A)=a\wedge b\) is syntactically more compact than the equivalent \(A\wedge B=a\wedge(a\lor b)\). Despite the fact that many redundancy removal techniques could be used to perform simplification under a care set, e.g., latch correspondence, signal correspondence and equivalence to constants, most of them are too expensive to be performed at each forward traversal iteration within an ITP scheme. For the sake of having a fast operator, simplify is limited to the removal of equivalences between state variables, i.e., _latch correspondences_. Given a target formula \(B\) and a care set \(A\), the Simplify operator identifies pairs of state variables \((v_{1},v_{2})\) such that \(A\rightarrow(v_{1}\leftrightarrow v_{2})\) and then \(B\) is simplified as \(B[v_{1}\gets v_{2}]\).