Why it matters

A property on one channel of a four-channel block took as long as a property on the whole block. The engineer assumed the tool looked only at the channel, but the channels shared twenty flops of control (illustrative numbers) and the proof correctly included them. Until the team could compute the cone by hand on a small example, every runtime argument was guesswork. This lesson is that hand computation.

Job of this lesson: define the cone as the transitive fan-in through next-state functions, computed per property, and scale it to the four-channel example.

The core idea

Start from the flops the property reads. Add every flop and input that can affect them through the next-state functions, and every gate on the way. Repeat until nothing new is added. That fixpoint is the cone of influence of that property: different properties on the same design have different cones, and only the cone matters to the run. Shared logic belongs to every cone that touches it, which is why the channel property paid for the shared control.

Worked example: a dozen nets by hand

Each net maps to the nets its next state or its logic reads. Five nets are flops (q0, q1, c0, x0, x1), three are inputs, five are gates. The property reads two flops; the fixpoint adds their drivers and stops. The check is applied to the netlist and then to a copy with one edge dropped, a no longer reads x0: x0 is reached only through that edge, so the cone shrinks and the check catches it. The same cone function then counts flops for the four-channel block (illustrative sizes: four channels of 100 flops and 20 shared flops).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

inputs = {"req", "gnt", "mode"}
flops = {"q0", "q1", "c0", "x0", "x1"}
fanin = {
    "q0": ["d0", "c0"], "q1": ["d1", "c0"], "c0": ["req", "gnt"],
    "d0": ["a", "sel"], "d1": ["b", "sel"],
    "a": ["x0"], "b": ["x1"], "sel": ["mode"],
    "x0": ["mode"], "x1": ["mode"],
    "req": [], "gnt": [], "mode": [],
}

def cone(netlist, reads):
    seen, frontier = set(), list(reads)
    while frontier:
        n = frontier.pop()
        if n not in seen:
            seen.add(n)
            frontier.extend(netlist[n])
    return seen

def check(netlist):
    both = cone(netlist, ["q0", "q1"])
    assert len(both) == 13 and len(both & flops) == 5 and len(both & inputs) == 3
    narrow = cone(netlist, ["q0"])
    assert narrow == {"q0", "d0", "c0", "a", "sel", "req", "gnt", "x0", "mode"}
    assert len(narrow & flops) == 3 and narrow < both

check(fanin)
mutant = dict(fanin)
mutant["a"] = []
assert cone(fanin, ["q0", "q1"]) - cone(mutant, ["q0", "q1"]) == {"x0"}
caught = False
try:
    check(mutant)
except AssertionError:
    caught = True
assert caught

def channel_cone(touched, per_channel=100, shared=20):
    return touched * per_channel + shared

assert channel_cone(4) == 420 and channel_cone(1) == 120 and channel_cone(0) == 20
assert 2 ** channel_cone(4) // 2 ** channel_cone(1) == 2 ** 300
print("PASS: cones of 13 and 9 nets (5 and 3 flops); a dropped edge loses x0 and is caught; one channel faces 120 of 420 flops")

The cone of one channel faces 2 to the 120 against 2 to the 420 for the whole block, a ratio of 2 to the 300. On the running FIFO the range check reads only count, a cone of 3 flops, while the tracked-data check also reads the memory and the pointers. Report the cone size per property: it should match the expected logic.

What the review looks for

• The cone is defined as transitive fan-in through next-state functions, per property, and shared logic is counted in every cone that touches it.

• Cone sizes are quoted per property and match the expected logic.

• No claim is made that the tool looks at anything outside the cone.

Verify and debug

Recompute the cone by hand on the schematic for any property whose runtime surprises you: the usual surprise is shared control you forgot. When a property passes instantly, read its cone before celebrating; an empty cone means a disconnected assertion, covered in the third lesson of this topic.

Related topics

• Next: COI Reduction Is Exact

• Later: Abstraction Techniques