Every property sees only part of the design: the registers it reads and everything that can reach them. That slice is the cone of influence, and it decides how hard the proof is. This topic defines the cone exactly, shows that removing what lies outside it cannot change a result, shows how to read a suspiciously small cone, and prices the cone in states and clauses.
Lesson | After it you can... |
|---|---|
Compute a property's cone on a small netlist and scale the idea to channels. | |
State why cone reduction cannot over-constrain, and separate it from assumptions and abstraction. | |
Spot an empty or tiny cone and prove the property is checking nothing. | |
Convert cone size to state space and unrolled clauses, and say when the cone is not enough. |
Suggested order: top to bottom. The first lesson defines the cone, the second shows reduction is safe, the third turns the size into a diagnostic, and the fourth turns it into arithmetic.
The property is disconnected from the design: it checks nothing. An instant pass with an empty cone is evidence of a wiring mistake, not of correctness.