October 25, 2004
Assertion Based Verification
Please note that contributed articles, blog entries, and comments posted on EDACafe.com are the views and opinion of the author and do not necessarily represent the views and opinions of the management and staff of Internet Business Systems and its subsidiary web-sites.
In October of 1991 a storm stronger than any in recorded history hit the coast off of Gloucester, Massachusetts. This "Perfect Storm" - so called because it was three storms combined into one - created an almost apocalyptic situation in the Atlantic ocean, where boats encountered waves of 100 feet. This was the basis of a film by the same name. It may not qualify as a perfect storm but something is happening on the EDA sea with the convergence of a need, technology and standards.
First, the need. Much, perhaps too much, has been written about the dramatic increase in the complexity of IC's by any available metric. This situation has ramifications for all aspects of the product lifecycle: design, verification, fabrication and test. EDA tools now enable design teams to generate designs that can not be truly verified in anything like a reasonable time. Many articles cite the fact that 70% of the time is spent in verification. The traditional black box approach to verification is to provide a set of input test vectors to a design simulation and monitor the actual output against the intended output. The test bench consists of a combination of cases that reflect the
specification, worry cases and random inputs. Unfortunately, even rather simple designs can require an enormous number of test vectors and therefore simulation time to exhaustively test for all possible combination of inputs. Consider the case of a simple 32 bit comparator which would require 264 vectors to exhaustively evaluate. Eliminating redundant and illegal inputs from test benches to reduce the number of vectors is itself a major challenge. A second shortcoming of simulation is that internal errors may never propagate to the outputs making them unobservable. Even if the effects do reach the output, it may be very difficult to trace the effect backwards to their cause.
Lastly, certain types of implementations errors are difficult to stimulate with functional tests. These are referred to as verification hot spots. There is a lack of control, i.e. an inability to activate, stimulate or sensitizes a specific point within the design. The consequence of these observability and controllability limitations is that a chip may require an expensive (~$1M) re-spin or worse a field recall due to design flaws undetected during the verification stage. According to well publicized study by Collet International Research, Inc 70% of designs requiring multiple respins have logic flaws.
Another issue with simulation is coverage. How do we know that the verification process is complete? There is both functional or specification coverage and implementation coverage. Metrics for the later include toggle coverage, code coverage (line, branch and sub-expression coverage), and finite state machine (FSM) coverage (state, arc and path). While easy to measure, it is difficulty to correlate these measures with coverage of functional intent. Functional coverage metrics, including coverage points, are designed to check that the verification tests have exercised specific key functionality - for example, executing all instruction types or transmitting and receiving all packet
types. However, functional coverage on the chip inputs and outputs may miss the exercise of the internal structures likes FIFIOs.
Next, the technology: Assertion Based Verification (ABV). Assertions capture the design intent. They specify both legal and illegal behavior of a circuit structure. The basic ABV method compares the implementation of a design against its specified assertions by embedding assertions in a design and having them monitor design activities. Assertions are placed wherever the protocols may be misused, assumptions violated, or design intent incorrectly implemented. Whenever an assertion is violated, it is reported immediately without the requirement for the problem to propagate to the design's outputs. One can also insert protocol assertion monitors to check for violations of the corresponding
interface protocols. Generally, there are two kinds of assertions. Concurrent assertions state that a given property must always be true throughout a simulation, while procedural (sometimes called temporal) assertions apply only for a limited time, or under specified conditions.
ABV can also be combined with formal verification techniques. Formal verification uses mathematical techniques to prove some assertions true (given a set of assumptions) and other assertions false (by discovering counterexamples). A proof means that static formal verification has exhaustively explored all possible behavior with respect to the assertion and has determined it cannot be violated. A counterexample shows the circumstances under which the assertion is not satisfied.
One can also produced a bounded proof as measured by a proof radius. The proof radius of an assertion is the number of cycles of design operation from an initial state that are covered by exhaustive formal analysis. Within the proof radius, the formal analysis guarantees that the assertion cannot be violated using any legal input sequence.
Proof radius is an assertion-based coverage metric that suggests whether the design needs more assertions. Assertion density measures the number of assertions of each type in each module. Minimum sequential distance measures the minimum number of levels of sequential logic from a given register to any assertion. Together, these metrics give the development team guidance about where to add more assertions.
0-In Design Automation identifies the fundamental technologies and methodologies (“pillars”) that make the ABV process successful.
Assertion-Based Verification provides benefit to users by:
In a paper from DAC in 1996 DEC revealed that a third of all bugs found in their Alpha microprocessor were detected by assertions.
the organization responsible for driving these standards.
You can find the full EDACafe event calendar here.
To read more news, click here.
-- Jack Horgan, EDACafe.com Contributing Editor.
Be the first to review this article