Every comparison endpoint is a key point. Primary inputs feed cones, primary outputs end them, and register outputs cut sequential feedback into combinational pieces.
A cone with no key point at its boundary cannot be checked in isolation. The boundary set must be complete before the run starts.
Key point | Role | If missing |
|---|---|---|
Primary input | Shared stimulus for both sides. | Cones start at different logic and agree by accident. |
Register output | Cuts feedback so the remaining logic is combinational. | Sequential loops enter the cone and the proof does not apply. |
Primary output | Observed result of each cone. | A divergence escapes unobserved. |
Memories, analog blocks and third-party macros are boxed: their internals are skipped. Each box becomes an ideal boundary with the same ports on both sides.
Boxing trades coverage for capacity. Logic inside a box is trusted, never proven.
Situation | Treatment | Consequence |
|---|---|---|
SRAM macro | Box with identical ports both sides. | Address decode and wrapper logic still compare. |
Analog block | Box at its digital interface. | Only the digital handshake compares. |
Unmapped hard block | Box until a model exists. | Its cone endpoints move to the box pins. |
Tie-offs must match on both sides of every key point. A pin tied to 1 in RTL and left floating in the netlist is a real divergence, not tool noise.
The same holds for box pins. Constant straps on a boxed macro are part of the comparison.
Boundary | RTL | Netlist must show |
|---|---|---|
Mode pin | Tied to 1. | The same constant 1. |
Box enable | Driven by logic. | The same driver cone, not a strap. |
Unused input | Tied to 0. | The same constant 0. |
Yes. The wrapper is outside the box, so its cones compare as usual. Only the macro interior is skipped.
Yes. Constants are compared values. The cones genuinely differ on every vector using that pin.