Using formal verification to check SoC connectivity correctness

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 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.

Types of point-to-point connectivity checks

Connectivity checking involves verifying device wiring. It’s asking the question: “Have the design elements been assembled correctly?” More precisely, it is verifying that the connections between blocks of logic in a design are correct, for example, that output A on block B1 is correctly connected to input A’ on block B2. This is often a difficult verification task. The physical number of connections to check is one issue, as designs contain thousands of wires which potentially all need to be checked for correctness.

Debugging presents a secondary though often equally challenging issue. The reason is that although checking the connectivity with dynamic tests using a directed or constrained random approach will certainly find some of the connectivity bugs, any problem will show up only as a functional issue inside the blocks under test, which doesn’t necessarily help in pinpointing the problem connection. Use of assertions may alleviate the debug problem by catching design errors at their source. However, the volume of checking required can still be staggering. In response to such challenges, formal verification offers us 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 Siemens Digital Industries Software 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.