Assertions Improve Productivity for All Development Phases

Assertions are increasingly important verification tools because they improve design quality and increase design verification (DV) productivity, resulting in faster time to market. Table 1 summarizes the different ways assertions contribute to the verification process.

Many qualities of assertions make them helpful during development phases other than DV. In fact, assertions can also improve productivity during the design and post silicon verification (PSV) development phases. This article discusses how assertions improve sandbox testing, PSV, and RTL coding.

Benefit of Assertions	How Achieved
Reduced debugging time	Pinpoint bugs at their source
Earlier bug detection	Find bugs that have not yet propagated to an output
Increased observability	Provide coverage statistics and insight into internal design events
Reduced coding and debugging time	Specify temporal behaviors more easily and concisely in a temporal language
Improved portability	travel with the RTL code of the design
Increased reusability	Execute in simulators and model checkers (formal verification)
Improved communication	Remove ambiguities present in natural language (English) descriptions

Table 1: The Benefits of Assertions

Assertions Improve Simulation-Based Sandbox Testing
Most assertion-based verification (ABV) methodologies dictate certain classes of assertions that should be written by the designer during the architecture and RTL coding phases. Usually, end-to-end design intent assertions are written during the architecture phase and RTL-level implementation assertions are written during the RTL coding phase.

To shorten the total development time, designers usually partially test their design before handing it off to the DV team. While the amount of designer testing varies across the industry, designers usually only ensure that the design resets, initializes, and processes a few basic transactions correctly. After this, the design is handed off to verification engineers who perform more detailed verification.

To perform this testing, a designer typically either builds a simple verification environment only capable of simple transactions (which we call a sandbox environment) or borrows the testbench written by the verification engineers, but constrains it to inject only simple transactions. Either way, the testing done by the designer is referred to as sandbox testing.

Assertions, both designer written and verification engineer written, help both sandbox approaches. Checker assertions help the designer quickly verify behaviors and pinpoint bugs. Assertions checking for unknown values (X and Z) are particularly useful while the design is being brought out of reset. Design-intent related assertions help the designer quickly verify the behavior of the design, bypassing the typical sandbox checking method of inspecting waveforms. Similarly, coverage assertions help the designer ensure each basic transaction is tested without having to study the waveforms.

Formally Verifying Assertions Further Improves Sandbox Testing
Since assertions have already been written for the design, why not eliminate the simulation-based sandbox testbench altogether? Why not formally verify the assertions instead?

Since formal tools automatically provide stimulus to prove assertions, no testbench is required. This saves the designer from having to create a sandbox environment and from having to learn how to drive the verification engineer's testbench. It also potentially yields a higher quality design before DV handoff since formal tools automatically verify simple and complex transactions, not just simple transactions.

A downside of model-checking is that constraints may be needed to remove illegal stimulus. While it may appear that adding constraints is analogous to building the throw-away sandbox environment that this approach intends to eliminate, these constraints are actually just additional assertions about the input signals of the block and are useful elsewhere as well. They can pinpoint testbench bugs during DV and are useful as output assertions for the driving block, so they are likely to be re-used elsewhere.

In the past, formal tools were not appropriate for sandbox testing because they reached state space explosion too quickly and were hard to use. In recent years, both problems have been overcome.

First, the capacity of modern tools is remarkably improved from years past due to numerous advancements, including automatic reduction and abstraction techniques. Additionally, bug hunting algorithms - algorithms tuned for finding bugs rather than exhaustive proofs - are now common. Bug hunting algorithms have much larger capacities than proof algorithms and are appropriate for sandbox testing since the goal is higher design quality at verification handoff, rather than exhaustive proofs.

Second, formal tools have become simpler to use for non-formal experts. They are now "push button" for problems that required dedicated formal experts in the past. While most have features used only by experts, these advanced features are not required to obtain good results. The tools are now simple enough that new users can become productive quickly.

Designers may prefer testing with formal tools because it lets them take advantage of the assertions they are writing anyway as part of an ABV methodology. It also saves them from having to build a throw-away sandbox environment. Since formal tools generate stimulus automatically, they can start testing their design sooner than they would with a sandbox environment, thereby finding bugs faster. Formal tools also automatically try corner cases, so they find complex bugs that would never have been found with a sandbox environment. All of this leads to increased design quality before DV handoff, which results in a faster overall development schedule.

Figure 1 summarizes the productivity improvement obtained by sandbox testing. In this graph, productivity is measured by the number of bugs found within a period of time.

1. Formal-based sandbox testing yields productivity gains.

Assertions Improve Post Silicon Verification
Before silicon can be shipped to customers, its behavior needs to be verified. Functional bugs that were missed by DV could surface in silicon, and there are other electrical and manufacturable reasons why parts may not work properly even if there are no RTL or gate-level bugs. Signal integrity issues and environmental tolerances such as voltage and temperature margins may cause functional problems.

Verifying that the first samples of a design do not suffer from any of these problems is called post silicon verification (PSV). During PSV, testbenches written for functional verification may become difficult or impossible to use because the testbench language may not be portable to either a lab or system environment. If a bug is found in silicon and the team would like to reproduce it within the testbench environment, they must figure out how to generate similar stimulus within the testbench. This is not always easy since visibility is usually limited in the lab or system environment, making it unclear what stimulus needs to be generated.

When observability becomes an issue, assertions can help. Since assertions are generally synthesizable to state machines and pipelines, they can be put directly on silicon with the design. In fact, both checking assertions, which verify the behavioral correctness of the design, and coverage assertions, which monitor the behaviors exhibited, can be placed on chip. Coverage assertions can improve the observability of transactions being processed, while checker assertions can detect bugs directly in silicon, thereby shortening the normally long and hard debugging process that would be required otherwise.

Simulation accelerators and emulators have been synthesizing assertions to their hardware environments for years. However, these environments are used as simulation accelerators or for prototyping, not for synthesizing assertions directly into the actual fabricated part.

2. Assertions are loaded into a reconfigurable block.

Recently, tools have emerged which place FPGA-like reconfigurable logic blocks within the RTL of a design and synthesize assertions to them. As shown in Figure 2, the assertions are then loaded into the block via JTAG or a configuration and control interface. The assertions then run in silicon at speed. Assertion results return through the same configuration interfaces and are viewable in a debugging environment much like simulated assertions are visible in a waveform viewer.

The connectivity between the signals within the design and the reconfigurable block limits the visibility of assertions compiled to this block. While tools can do a reasonable job of guessing which signals should be connected, the designer may be able to optimize this list with manual intervention. The inputs to assertions written for ABV are a good place to start.

Similarly, the size of the reconfigurable block dictates the number and complexity of assertions that can be run in parallel in silicon. This yields a classic engineering trade off between the overhead of the gates fabricated just for assertions (i.e. just for debug) and the efficacy of the debugging block. With a little planning, the block can be sized to accommodate a useful subset of the assertions that were found most helpful during pre-silicon DV.

There is a high correlation between the assertions that proved useful pre-silicon and the assertions that will prove useful during PSV. However, there are usually at least a few assertions that were not written before tape-out, which will help debug new problems encountered in the real hardware. An advantage of loading assertions into reconfigurable blocks is that these new assertions can be used, provided that the block has sufficient resources to accommodate them. For this reason, it is prudent to size the reconfigurable block a little larger than would be needed just for a helpful subset of the assertions using during DV.