CAMUS Results - Reveal Benchmarks
These benchmarks were generated by Reveal, a tool for hardware equivalence checking developed by Zaher Andraus, operating on three different microprocessor designs. Reveal utilizes CAMUS to find all MUSes of instances generated within a counterexample-guided abstraction refinement (CEGAR) flow for verifying designs such as pipelined microprocessors. For more information, refer to our paper:
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 11th Asia and South Pacific Design Automation Conference (ASP-DAC-2006), pp. 19-24, January 2006.
The CNF in these instances was generated from high-level constraints in a first-order logic. Each high-level constraint is encoded as a large number of CNF clauses. CAMUS can make use of this information to group clauses by the constraint from which they were generated. It then treats each block of clauses as a single constraint, returning MUSes in terms of those high-level constraints. The number of groups defined for each instance is reported in the "Groups" column.
Results are reported for both using the group information and without using groups. A "--" runtime indicates that the 600 second timeout was reached. Statistics on the MCSes and MUSes produced are in terms of the high-level constraints for the "with groups" results. Runtimes for generating MUSes are not reported because they were negligible (a few milliseconds at most) in all cases.
| Using Constraint Groups | Without Constraint Groups | ||||||||||||||||||
| Runtime (sec) | MCS Sizes | MUS Sizes | Runtime (sec) | MCS Sizes | MUS Sizes | ||||||||||||||
| Name | Vars | Clauses | Groups | MCSes | #MCSes | Min | Max | #MUSes | Min | Max | MCSes | #MCSes | Min | Max | #MUSes | Min | Max | ||
| dlx_1 | 6804 | 78364 | 25 | 0.354 | 3 | 1 | 5 | 5 | 2 | 3 | -- | >806 | 3 | 4 | |||||
| dlx_2 | 6268 | 98290 | 23 | 0.335 | 2 | 1 | 2 | 2 | 2 | 2 | -- | >15305 | 1 | 4 | |||||
| dlx_3 | 5976 | 139141 | 18 | 0.587 | 2 | 1 | 4 | 4 | 2 | 2 | -- | >8158 | 4 | 5 | |||||
| dlx_4 | 12428 | 161242 | 16 | 0.568 | 2 | 1 | 2 | 2 | 2 | 2 | 7.88 | 327 | 2 | 3 | 3 | 3 | 39 | ||
| dlx_5 | 17951 | 54212 | 21 | 0.219 | 3 | 1 | 3 | 3 | 2 | 3 | -- | >280 | 2 | 3 | |||||
| dlx_6 | 30852 | 92213 | 54 | 0.816 | 9 | 1 | 9 | 9 | 2 | 3 | -- | >0 | |||||||
| dlx_7 | 36315 | 138197 | 15 | 0.391 | 2 | 1 | 1 | 1 | 2 | 2 | 1.25 | 39 | 1 | 1 | 1 | 39 | 39 | ||
| intel_1 | 1756 | 4634 | 7 | 0.129 | 7 | 1 | 2 | 2 | 5 | 5 | -- | >709 | 1 | 2 | |||||
| intel_2 | 3512 | 4634 | 7 | 0.091 | 6 | 1 | 2 | 2 | 4 | 6 | -- | >983 | 1 | 2 | |||||
| intel_3 | 1704 | 4222 | 7 | 0.009 | 2 | 1 | 1 | 1 | 2 | 2 | 0.029 | 39 | 1 | 1 | 1 | 39 | 39 | ||
| intel_4 | 3886 | 5402 | 9 | 0.014 | 2 | 1 | 1 | 1 | 2 | 2 | 0.047 | 39 | 1 | 1 | 1 | 39 | 39 | ||
| intel_5 | 6291 | 5976 | 10 | 0.016 | 2 | 1 | 1 | 1 | 2 | 2 | -- | >33017 | 1 | 5 | |||||
| intel_6 | 9481 | 8174 | 13 | 0.138 | 7 | 1 | 2 | 2 | 5 | 5 | -- | >887 | 1 | 2 | |||||
| intel_7 | 12671 | 8174 | 13 | 0.115 | 6 | 1 | 2 | 2 | 4 | 6 | -- | >1020 | 1 | 2 | |||||
| oc_10 | 29421 | 13405 | 23 | 0.079 | 3 | 1 | 2 | 2 | 3 | 3 | -- | >11038 | 1 | 3 | |||||
| oc_11 | 32089 | 6197 | 10 | 0.035 | 2 | 1 | 1 | 1 | 2 | 2 | 0.169 | 38 | 1 | 1 | 1 | 38 | 38 | ||
| oc_12 | 38401 | 18162 | 25 | 0.076 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >5908 | 1 | 6 | |||||
| oc_13 | 44396 | 17500 | 24 | 0.08 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >5310 | 1 | 4 | |||||
| oc_14 | 50708 | 18162 | 25 | 0.086 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >5136 | 1 | 6 | |||||
| oc_15 | 54039 | 10834 | 12 | 0.064 | 2 | 1 | 1 | 1 | 2 | 2 | -- | >2087 | 1 | 4 | |||||
| oc_16 | 58995 | 14916 | 19 | 0.076 | 2 | 1 | 1 | 1 | 2 | 2 | -- | >13894 | 1 | 6 | |||||
| oc_17 | 63153 | 12853 | 17 | 0.077 | 2 | 1 | 1 | 1 | 2 | 2 | -- | >1240 | 1 | 4 | |||||
| oc_1 | 6129 | 14717 | 25 | 0.053 | 4 | 1 | 2 | 2 | 3 | 4 | -- | >10074 | 1 | 3 | |||||
| oc_2 | 12124 | 17500 | 24 | 0.049 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >5855 | 1 | 4 | |||||
| oc_3 | 18436 | 18162 | 25 | 0.057 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >6032 | 1 | 6 | |||||
| oc_4 | 23959 | 13405 | 23 | 0.076 | 3 | 1 | 2 | 2 | 3 | 3 | -- | >11000 | 1 | 3 | |||||
| oc_5 | 30271 | 18162 | 25 | 0.066 | 3 | 1 | 1 | 1 | 3 | 3 | -- | >5301 | 1 | 6 | |||||
| oc_6 | 5093 | 18129 | 19 | 0.06 | 2 | 1 | 2 | 2 | 2 | 2 | -- | >2823 | 2 | 4 | |||||
| oc_7 | 11277 | 17696 | 24 | 0.083 | 3 | 1 | 4 | 4 | 2 | 3 | -- | >12 | 3 | 3 | |||||
| oc_8 | 17374 | 14685 | 25 | 0.072 | 4 | 1 | 2 | 2 | 3 | 4 | -- | >11484 | 1 | 3 | |||||
| oc_9 | 23898 | 18762 | 26 | 0.086 | 2 | 1 | 2 | 2 | 2 | 2 | -- | >2142 | 2 | 4 | |||||