# Hardware Model Checking Algorithms and Techniques
## 3 Bounded Model Checking  
Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant property \(P\), bounded model checking (BMC) [38] is an iterative approach whose purpose is to check whether a counterexample to \(P\) of length at most \(k\) in \(\mathcal{M}\) exists or to prove its absence. In order to carry this out, BMC simply performs a SAT check on a formula defined as follows. **Definition 83** (BMC Formula). : _A BMC formula of length \(k\) for \(P\) in \(\mathcal{M}\) is the propositional formula \(\textsc{bmc}(k)\) over \(V^{0}\cup\cdots\cup V^{k}\):_  
\[\textsc{BMC}(k)\stackrel{{\text{\tiny def}}}{{=}}\Pi_{0}(k) \wedge\overset{k}{\underset{i=0}{\overset{\tiny f}{\vee}}}\
eg P(V^{i})= \mathcal{I}\wedge Cone(0,k) \tag{44}\]  
Intuitively, a BMC formula of length \(k\) encodes all initial paths in \(\mathcal{M}\) of length at most \(k\) capable of reaching a bad state in \(\
eg P\). If the BMC formula is Sat, then there exists a counterexample to \(P\) of length at most \(k\) in \(\mathcal{M}\). Conversely, no such counterexample exists. BMC tools iteratively solve BMC formulas of increasing bound, until either a counterexample is found or some maximum bound is reached. Due to the way it operates, BMC is effective in finding counterexamples but it is not able to detect whether \(P\) holds in \(\mathcal{M}\). In order to surpass such a limitation, specific techniques are required to support unbounded model checking. The ability to check reachability fix-points and/or to find inductive invariants is thus the main difference, and additional complication, between BMC and UMC techniques, which will be introduced in the following sections. Figure 4: Different types of traces with respect to a given \(\mathcal{M}\stackrel{{\text{\tiny def}}}{{=}}\langle V,\mathcal{I },T\rangle\). Algorithm 2 reports the BMC procedure up to a certain bound \(k_{max}\). First, the algorithm checks whether the property \(P\) is satisfied by the initial states (lines 2-3). If an initial state fails to satisfy \(P\), the procedure terminates by returning Fail along with a trivial counterexample. Otherwise, the procedure starts iterating over increasing values of \(k\) up to \(k_{max}\), checking whether there is at least a path satisfying the BMC formula up to bound \(k\) (Definition 83) at each iteration (lines 6-8). If a satisfying path \(\pi^{0,k}\) is found, the procedure returns Fail along with the path as a counterexample. If the procedure does not find any counterexample of length up to \(k_{max}\), it returns a Success, indicating that \(P\) holds up to the given bound. ```
0:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\); \(k_{max}\) maximum bound. 0:\(\langle\mathit{res},\mathit{cex}\rangle\) with \(\mathit{res}\in\{\textsc{Success},\textsc{Fail}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample. 1:procedureBoundedModelChecking(\(\mathcal{M}\), \(P\), \(k_{max}\))
2:if\(\exists s_{0}\models\mathcal{I}(V)\land\
eg P(V)\)then
3:return\(\langle\textsc{Fail},(s_{0})\rangle\)
4:\(k\gets 1\)
5:while\(k\leq k_{max}\)do
6:\(\textsc{bmc}(k)\leftarrow\Pi_{0}(k)\land\bigvee_{i=0}^{k}\
eg P(V^{i})\)
7:if\(\exists\pi^{0,k}\models\textsc{bmc}(k)\)then
8:return\(\langle\textsc{Fail},\pi^{0,k}\rangle\)
9:\(k\gets k+1\)
10:return\(\langle\textsc{Success},-\rangle\)
```  
**Algorithm 2** Top-level procedure of the BMC algorithm. As explained above, the search for a counterexample of a given length is inherently incomplete, thus the need for additional techniques in order to overcome such a limitation. Nevertheless, BMC find application in several scenarios, due to its relative ease of application, both in hardware and in software model checking. The minimum requirement is being capable of encoding the transition relation of the instance at hand in a suitable way, e.g., a circuital representation.