Mark Liffiton

lastname -at- eecs -dot- -domain-

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:

Refinement Strategies for Verification Methods Based on Datapath Abstraction
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 GroupsWithout Constraint Groups
Runtime
(sec)
MCS SizesMUS SizesRuntime
(sec)
MCS SizesMUS Sizes
NameVarsClausesGroupsMCSes#MCSesMinMax#MUSesMinMaxMCSes#MCSesMinMax#MUSesMinMax
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