Assertion Synthesis

In June, Atrenta acquired NextOp, the leader in assertion synthesis. So what is it?

Depending on who you ask, verification is a huge fraction, 60-80%, of the cost of an SoC design, so obviously any technology that can reduce the cost of verification has a major impact on the overall cost and schedule of a design. At a high-level, verification is checking that the RTL corresponds to the specification. So it follows that without an adequate specification the debugging cycle will just drag out and the design and verification teams will be unable to have confidence that there are no bugs that will cause the chip to fail.

Assertion-based verification helps teams using simulation, formal verification and emulation methodologies, to accelerate verification sign-off. The RTL and test specifications are enhanced to include assertions and functional coverage properties. These are statements that define the intended behavior of signals in the design. Assertion synthesis automates the manual process of creating adequate assertions and functional coverage properties and so makes assertion-based verification more practical.

Modern verification includes a mixture of directed simulation, constrained random simulation, formal verification and emulation. Directed simulation, where the output is explicitly tested for each feature, does not scale for large designs. Constrained random, where an external checker model of the design is used and the output of the RTL checked against the checker, suffers from incompleteness of the checker (since it is so hard to write). Assertion-based verification enhances all these approaches, supplementing the existing checkers with assertions about the internal logic. They thus inject observability into the RTL code. Often features that are hard to verify only looking at the outputs of the RTL are often easy to check using assertions about the internals.

But the challenge of assertion-based verification is creating enough assertions when they must be created manually. Generally one assertion is needed for every 10 to 100 lines of RTL code but it can take hours to create, debug and maintain each assertion. Assertion synthesis is technology that automatically creates high quality assertions to capture design constraints and specifications, and creates functional coverage properties that expose holes in the testbench.

Here’s how it works. Engineers use the RTL and test information as input to BugScope, which automatically generates properties that are guaranteed to hold for the given stimulus set. The new coverage properties provide evidence of holes the the verification does not cover, and the assertions provide observability into each blocks targeted behavior, which, if triggered, indicate design bugs. The assertions are then used with verification tools such as simulators, formal verification engines and emulation. Additional stimulus can be generated to patch coverage holes.

As these steps are repeated, the number of coverage properties (indicating holes in coverage) will decrease and, at verification sign-off, will have been replaced exclusively by assertions.

The Atrenta whitepaper on Assertion Synthesis, which includes more detail and a case-study, is here.