Lesson 2.3 · How Formal Engines Think

The cone of influence

Before any heavy math, every formal tool performs a simple but powerful reduction: it walks backwards from the signals mentioned in a property, through combinational logic and flops, and collects everything that can possibly influence them. This is the property's cone of influence (COI). Everything outside the cone is discarded for that proof.

The cone (shaded) contains only the logic that can affect the property. Inputs and flops outside it are removed before proving.

Why you should care

The size of the COI — especially the number of state bits in it — is one of the best early predictors of proof difficulty. Two practical consequences:

Prefer local properties. "The output FIFO never overflows" may only involve a few counters, while "every packet that enters eventually leaves with the right data" can pull in the whole block.
Read the tool's COI report. Most tools report how many flops are in the cone of each property. A surprise — say 5,000 flops for a simple handshake property — usually means an unintended dependency, such as a wide data bus reaching the property through a parity check.