In these examples, the component being verified handles off-chip communications (particularly the interactions between the cache-coherence protocol and second-level data cache). The structure has had a number of reductions applied, particularly symmetry and cone-of-influence. The design's initial states and free inputs have been constrained to take on only legal values. The properties being verified are small, fairly local invariants -- there are several hundred such properties to verify of this component, and together they still don't constitute a full verification.
The archive bmc-alpha-2001-06-26.tar.gz should expand into a directory called bmc-alpha, containing these files:
| # | File Name | Description | k | Variables | Clauses |
| 1 | bmc-alpha-25449.cnf | cache coherence and control | 30 | 663443 | 3065529 |
| 2 | bmc-alpha-4408.cnf | cache coherence and control | 40 | 1175403 | 3054591 |
| 3 | bmc-alpha-12225.cnf | cache coherence and control | 60 | 1754536 | 4565530 |
| 4 | bmc-alpha-17181.cnf | cache coherence and control | 65 | 1904628 | 4956141 |
The number of clauses and variables is affected by the very simple-minded translation of the problem from a network of logic gates, which produces only clauses of length two or three. A slightly more parsimonious translation is possible.
Tim Leonard Formal Design Verification Alpha Development Group Compaq Computer Corporation