# Hardware Model Checking Algorithms and Techniques
## 8 Comparative Analysis and Experimental Evaluation  
In order to compare and evaluate the various model checking algorithms, we here present the data gathered taking into account our own implementation of said techniques on top of the PdTRAV tool [56], a state-of-the-art model checking academic tool. The benchmark set considered was derived from past HWMCC suites [14; 57], starting from the 2014 edition until the most recent one. The set includes hardware- as well as software-derived verification problems, mostly stemming from industrial-level verification instances (such as IBM and intel benchmarks). Experiments were run on an Intel Core i7-1370, with 16 CPUs running at 3.4 GHz hosting a Ubuntu 22.04 LTS Linux distribution. All the experiment were run taking into account a time limit of 3600 s and a memory limit of 32 GB. Experimental results are reported in Tables 1 and 2, which share the same structure. Both tables highlights solves, split between SAT and UNSAT instances (Result), for each main engine (Engine) of our verification suite. For each group of results, we provide the average number of memory elements (\(avg_{I}\)), input variables (\(avg_{i}\)) and gates (\(avg_{g}\)) of the benchmarks belonging to each set, to provide some insight into the size of the instances at hand. As summary statistics, we also provide average solving time, both in term of CPU time (\(avg_{t}\)) and wall-clock time (\(avg_{r}\)), and memory requirements (\(avg_{m}\)) for each group. Table 2 provides a subset of the results of Table 1, filtering out easier instances, i.e., instances that require 60 seconds or less to be solved. \begin{table}
\begin{tabular}{c c c c c c c c} \hline \hline
**Engine** & **Result** & **Solutions** & \(avg_{i}\) & \(avg_{t}\) & \(avg_{g}\) & \(avg_{t}\) [s] & \(avg_{g}\) [s] & \(avg_{m}\) [MB] \\ \hline \multirow{3}{*}{BDD} & SAT & 12 & 16.25 & 307.33 & 9458.17 & 1014.53 & 175.71 & 1518.29 \\  & UNS & 91 & 83.81 & 222.68 & 2723.90 & 1959.57 & 353.31 & 1921.69 \\ \multirow{3}{*}{BMC} & SAT & 185 & 5811.45 & 16,011.02 & 201,773.13 & 1409.58 & 330.53 & 3314.58 \\  & SAT & 1 & 122.00 & 381.00 & 2526.00 & 0.59 & 0.69 & 58.60 \\ \multirow{3}{*}{COR} & UNS & 121 & 6500.72 & 24,608.60 & 215,393.50 & 28.80 & 29.16 & 462.13 \\  & UNS & 32 & 1367.50 & 1463.75 & 29,644.44 & 3359.04 & 657.87 & 4796.34 \\ \multirow{3}{*}{ITP} & UNS & 86 & 2728.55 & 6079.29 & 74,085.93 & 3294.79 & 670.03 & 3923.90 \\ \multirow{3}{*}{LMS} & UNS & 19 & 47.26 & 584.32 & 3687.63 & 731.97 & 124.60 & 1464.49 \\  & SAT & 43 & 579.37 & 1188.88 & 18,866.86 & 496.82 & 95.26 & 1482.05 \\ \multirow{3}{*}{PDR} & UNS & 233 & 558.95 & 3599.55 & 36,061.80 & 462.56 & 97.19 & 1792.21 \\ \multirow{3}{*}{RED} & UNS & 2 & 203.00 & 271.00 & 4840.00 & 1.54 & 2.64 & 113.35 \\ \multirow{3}{*}{SIM} & SAT & 36 & 1011.22 & 4596.92 & 45,924.17 & 224.19 & 78.73 & 1742.41 \\ \multirow{3}{*}{SYN} & UNS & 91 & 596.62 & 819.20 & 14,008.29 & 10.36 & 7.69 & 395.29 \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Results on the full benchmark set of the number of instances solved by different engines. In the tables one can find both SAT-based model checking techniques, which are the focus of this paper, such as IC3 in its PDR variant, BMC, induction-based approaches exploiting lemmas (LMS), interpolation and IGR, as well as some solutions obtained through auxiliary techniques, such as BDD-based reachability, logic synthesis, simulation and combinatorial techniques to circuit manipulation and checking, which go past the scope of the current work. It is worth remembering that the portfolio-based approach awards the solution for a specific instance to the first engine capable of solving the corresponding verification task, for the sake of efficiency. In such a scenario, after (at least) one engine manages to solve a problem, all the concurrent running task are brought to a halt, in order to spare resources.