Why it matters

Two properties on the same block differed in runtime and nobody could say why: one saw 120 flops, the other nearly the whole 420 (illustrative). The tempting answer is the exponent, 2 to the 120 against 2 to the 420, but that number bounds a different thing from solver time. This lesson prices the cone in two honest numbers, states what each bounds, and says what neither predicts.

Job of this lesson: convert cone size to state space and to unrolled problem size, and state when cone reduction alone is not enough.

The core idea

A cone of C flops has at most 2 to the C states, which bounds an explicit enumeration. A bounded check unrolls the cone: each step adds a copy of its gates, and a two-input gate costs about three clauses, so gates times three times depth, plus one equality per flop per step, bounds the memory of the check. Neither number predicts the time the solver takes: that depends on the property and on the structure of the logic. Measured on the running designs, the skid stage at depth 25 takes 0.26 s with its helper invariants and 4.5 s without them (the tracked-word property is the slow part).

Worked example: from flops to clauses

The first script derives the channel numbers from the sizes (illustrative: four channels of 100 flops, 20 shared) and checks the ratio 2 to the 300, about 2.0 times 10 to the 90, and the case of a property on the shared control only. A function that forgets the shared flops is caught by the same check.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

import math

def cone_flops(touched, per_channel, shared):
    return touched * per_channel + shared

def check(fn):
    total, one, two, shared_only = fn(4, 100, 20), fn(1, 100, 20), fn(2, 100, 20), fn(0, 100, 20)
    assert (total, one, two, shared_only) == (420, 120, 220, 20)
    exponent = total - one
    assert exponent == 300
    assert 2 ** total // 2 ** one == 2 ** 300
    assert abs(10 ** (exponent * math.log10(2) - 90) - 2.04) < 0.01

check(cone_flops)
caught = False
try:
    check(lambda touched, per_channel, shared: touched * per_channel)
except AssertionError:
    caught = True
assert caught
print("PASS: cones of 120 and 420 flops differ by 2 to the 300, about 2.0e90; a model that forgets the shared flops is caught")

The second script prices an unrolled problem for illustrative sizes: 50,000 gates and 2,000 flops at depth 30 give 4.5 million gate clauses plus 60,000 flop links; at depth 300 the gate clauses are 45 million. The check is applied to the formula and to three mutants (no flop links, no factor of three, a missing depth factor), each caught.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

def unrolled(gates, flops, depth):
    return gates * 3 * depth + flops * depth

def check(fn):
    assert fn(50000, 2000, 30) == 4500000 + 60000
    assert fn(50000, 2000, 300) == 10 * fn(50000, 2000, 30)
    assert fn(50000, 0, 300) == 45000000
    assert fn(0, 2000, 30) == 60000

check(unrolled)
mutants = [
    lambda g, f, d: g * 3 * d,
    lambda g, f, d: g * d + f * d,
    lambda g, f, d: g * 3 + f * d,
]
for mutant in mutants:
    caught = False
    try:
        check(mutant)
    except AssertionError:
        caught = True
    assert caught
print("PASS: 4.56M clauses at depth 30 and 45.6M at depth 300; all three mutants are caught")

Linear growth with depth means a deep bounded check is limited by memory first on a big cone, and the next move is to narrow the cone, abstract, split the property, or strengthen it with a helper invariant (all taught later), not to read the exponent as a runtime forecast.

What the review looks for

• Cone sizes converted to state space and unrolled problem size before any runtime argument; sizes marked illustrative unless measured.

• Shared logic identified as the floor, and the next step named when the cone is still wide: abstract, split, or strengthen.

Verify and debug

When a run stalls, recompute both numbers and compare the properties' cones, then change one thing at a time: narrow the property, abstract the shared block, or add the helper. Never read a stalled run as a verdict on the design.

Related topics

• Earlier: Reading Cone Size per Property

• Later: Abstraction Techniques