A property on one output channel of a four-channel block proves quickly, and the report shows full line coverage of the file. But three channels never influenced the proof, and an entire debug block sits outside every cone. Cone coverage would have shown the gap in one table; line coverage hid it. This lesson defines both terms precisely and computes them on a small netlist you can check by hand.
The cone of influence of a property is the set of registers and inputs that can affect the checked signals, traced backwards through combinational logic and one step per cycle of history. It is exact: cone reduction removes only logic that cannot affect the property, and it never over-constrains; over-constraint comes from assumptions, which are a different thing. Coverage over proven properties is the union of their cones divided by the design: logic in no cone was never examined by any proof.
The proof core is smaller: the subset of the cone the proof actually needed. A solver may discharge a property using only part of the cone, for example when a case split makes one path irrelevant. Reporting the core beside the cone shows how much of the possible dependence the proof exercised. A high cone coverage with a shallow proof depth is not strong evidence, as the last lesson of this topic shows.
An illustrative seven-block design: blocks b0 to b2 read three inputs and feed the shared block b3, b3 feeds b4, and a separate chain b5 then b6 reads a fourth input. Three properties check the outputs of b4, b6 and b3. The script computes each cone by backward reachability, checks that each proof core sits inside its cone, and reports the union coverage. Then it injects an eighth block, a debug counter that only reads other blocks and drives no checked output, and the coverage drops from 7 of 7 to 7 of 8.
# illustrative: cone and proof-core coverage on a small netlist
# blocks and what each block reads (fan-in); outputs checked by p1..p3
fanin = {"b0": ["in0"], "b1": ["in1"], "b2": ["in2"], "b3": ["b0", "b1", "b2"],
"b4": ["b3"], "b5": ["in3"], "b6": ["b5"]}
checked = {"p1": "b4", "p2": "b6", "p3": "b3"}
def cone(net, out):
seen, stack = set(), [out]
while stack:
x = stack.pop()
if x in seen:
continue
seen.add(x)
stack.extend(net.get(x, []))
return {b for b in seen if b in net}
def coverage(net):
cones = {p: cone(net, o) for p, o in checked.items()}
union = set().union(*cones.values())
return cones, union, len(union) / len(net)
def cores_ok(cores, cones):
return all(cores[p] <= cones[p] for p in cones)
cones, union, cov = coverage(fanin)
assert cones["p1"] == {"b4", "b3", "b0", "b1", "b2"}
assert cov == 1.0
# proof cores: the subsets the (illustrative) proofs actually consumed
cores = {"p1": {"b4", "b3", "b0", "b1"}, "p2": {"b6", "b5"}, "p3": {"b3", "b0", "b2"}}
assert cores_ok(cores, cones)
# a core outside its cone means the bookkeeping is wrong: the check must catch it
assert not cores_ok(dict(cores, p2={"b6", "b2"}), cones)
# inject an unobservable debug block: it reads b4 and b6 but drives no checked output
with_dbg = dict(fanin, dbg=["b4", "b6"])
cones2, union2, cov2 = coverage(with_dbg)
assert abs(cov2 - 7 / 8) < 1e-9
assert set(with_dbg) - union2 == {"dbg"}
print("PASS: cone coverage 7/7, then 7/8 with injected block dbg uncovered; bad core rejected")The debug block sits in no cone: no property can see it. The fix is a property on its outputs or a documented reason it needs none, never a wider netlist. The subset check runs in one direction on purpose: a core outside its cone means the bookkeeping is wrong, not that the proof saw more, and the script shows the check rejecting such a table.
Every property reports its cone size, and the size matches the expected logic: a surprise means a disconnected check or a missing path.
The union coverage names each uncovered block, and each has a property or a written reason.
Core and cone are both reported; a core much smaller than its cone invites the question of what was left unexercised.
A property that proves instantly with an empty or tiny cone is disconnected: the checked signal was optimised away, the hierarchy path is wrong, or an unused signal is named. Mutate a signal inside the expected cone and rerun: if the property still passes, the cone report was telling the truth and the property looks elsewhere. Always confirm the cone before celebrating the speed.
Both can see the same logic, but one proof exercised much less of it. The small-core property deserves a harder look: a case split or an assumption may have excused most of its cone without anyone noticing.