Using Formal Verification to Check SoC Connectivity Correctness

ABSTRACT

Formal verification offers a solution that is quick, exhaustive and allows for efficient debug. It’s true that traditionally, chip-level formal verification is impractical. The approach usually targets the block level to keep the size of the state space to an appropriate level. But given that connectivity checking is focused solely on the wiring — which is generally a simple part of the device, compared to the complexity found at the block-level — the state space can with some assumptions be reduced to a manageable size. The nature of this simplification depends on the type of checking that is required. After first outlining several types of connectivity checks, this paper then provides details, including code, of a new semi-automated verification flow used by several Mentor Graphics customers to simplify connectivity checking. The flow is based on a script-based environment, about which sufficient information is provided to begin implementing the new verification approach.