Assertion
Processor
Table of Contents
The Verification Challenge
Many are predicting that assertions are the next big breakthrough
that will enable engineers to continue to design and verify larger
and more complex designs. Assertion-based methodologies will bring
much needed structure to the current set of ad-doc testbench and
monitoring techniques used by most projects for simulation as well
as enable more widespread adoption of emerging formal and semi-formal
verification technologies.
As today's designs push past 1M gates and move
toward 10M gates, engineers require new tools and methodologies
to verify these devices. Unfortunately, some engineers expect to
verify these chips using the same waveform dumps, ad-doc testbench
code with $display statements, and scripts with log file greps to
monitor simulation results. What is needed is a common methodology
that will propel the use of assertions across a wide variety of
tools ranging from formal verification to logic simulation to emulation.
This common methodology will provide increased automation and enable
the full benefit of the write once characteristic of assertions.
Axis is participating in making this vision a reality by educating
engineers on the value of assertion-based verification and making
sure assertion-based methodologies work well with its simulation,
simulation acceleration, and emulation products. The combination
of assertions with the general-purpose RCC verification platform
for simulation, simulation acceleration, and emulation will provide
users with the needed performance and debugging to meet verification
requirements for the next generation of designs.
Introduction to Assertions
Assertions document the designer's assumptions and the properties
of the design. They are a powerful tool to crosscheck the design's
actual versus intended behavior. They are also valuable to verification
and system engineers to formally specify the intended behavior of
the system and to make sure it is acting according to specification.
Recently, much has been written about assertions and even though
the concept has existed for years there is still much confusion
over assertions. Before getting into the details of how assertions
are specified and implemented it is useful to look at the motivation
behind why assertions are so important.
Assertions provide a common format for
multiple tools. Without an agreed upon method of specifying
assertions there is no chance to automate activities such as functional
coverage metrics, error reporting, and severity levels. A common
assertion methodology lends itself to increased automation in both
formal verification and simulation. Assertions can also benefit
from a "write-once, run-anywhere" characteristic. Once
inserted into a design they can be used by many tools and are quite
portable for design reuse.
Assertions are better than a paper test
plan. Verification involves deriving a list of features
to be tested from the design specification. Most projects write
a test plan that dictates how the features of the design are to
be verified. These features are then documented and a testcase is
developed to verify each feature. Testcases usually take the form
a testbench that will cause the desired feature to be exercised.
This directed approach is commonly augmented with random testing.
Assertions help to automate the manual process of running a testcase;
visually verifying the test has covered the feature, and adding
the test to the regression suite. Without using assertions there
is often no way to guarantee the testcase still exercises the feature
as the design evolves. Assertions provide a mechanism to measure
functional coverage and quantify test results.
Assertions ease debug and reduce simulation
time. One of the main motivations for assertions is reduced
debug time. Since assertions are a white-box verification technique
they provide increased visibility and controllability of the design
under test. Assertions will detect design errors as soon as they
occur without waiting for the effects to be propagated to the device
or system boundaries. Having an immediate indication of a problem
can save hours of trying to look backward to get to the root cause
of the problem. The use of assertions has been reported to reduce
debug time by as much as 50% [1]. Assertions can also save simulation
time since they can terminate a simulation when a fatal error occurs.
A runaway or meaningless simulation can waste valuable simulation
time if it occurs during an overnight regression run when more tests
could be given a chance to run.
Assertions verify interfaces between
blocks. During integration phases assertions act as watchdogs
at the module or block interface boundaries making sure each block
obeys the agreed upon protocol. This can be crucial since it is
possible for a testcase to pass based on the data observed at the
chip or system boundaries even when there is a violation of a protocol
inside the design. Assertions help eliminate such situations.
Assertions are a good RTL coding practice.
Assertions are far more valuable than comments alone in the design.
Well-commented code makes it easier to maintain and to understand
the intended functionality. Assertions go one step further by documenting
exactly what the code is expected to do in a way that can be verified
using tools instead of a human reading the comments and attempting
to understand if the code is working correctly. Assertions are also
a good way to sanitize the code before check-in. Tools can read
a design file and its assertions and indicate possible problem areas.
In the same way a lint program checks for errors in the code's syntax
and structure, assertions can be used to check for errors in the
designs behavior.
Assertions provide many benefits to system-level
engineers, design engineers doing RTL coding, and verification engineers.
Each group brings different knowledge about the design and its operation,
but a common assertion methodology allows all parties to benefit.
Assertion Definitions
To understand more details of an assertion-based methodology a common
set of definitions is presented.
Property: A general behavioral attribute
used to characterize a design. Properties can be high-level attributes
such as characteristics of incoming and outgoing networking packets
or low-level attributes related to the state encoding of a finite
state machine (FSM).
Event: An occurrence of a desirable behavior.
Observing events are required as part of verification to ensure
completeness. Measuring the occurrence of events leads to quantitative
data about specific corner cases and other properties of the design
have been verified. Statistics about events lead to functional coverage
metrics.
Assertion: An assertion is a statement
about a specific property that is expected to be true for the design.
Assertions are usually used to trap undesirable behavior. Assertions
are checkers and monitors used to enforce rules and assumptions
about the design.
Static: An event or assertion that is
true for all time or is only checked at a specific instance of time.
No knowledge of previous history of the design state is required.
Temporal: An event or assertion that
spans a sequence of time. History is required to track the sequence
over time.
Procedural Assertion: An assertion that
is described within the context of an executing process or set of
sequential statements such as a VHDL process or a Verilog always
block. The assertion will be evaluated based on the path taken through
the set of sequential statements.
Declarative Assertion: An assertion that
exists within the structural context of the design. It is evaluated
along with all of the other structural elements in the design. For
example a module that takes the form of a structural instantiation.
Regular Expression: A regular expression
is a way to express how a computer program should look for a specified
pattern and how to react when matching patterns are found. A common
use of regular expressions is found in the UNIX grep tool. Specification
of properties is easily done by the use of regular expressions.
This explains why languages like PERL are used in design verification
applications.
Property Language, Declarative Language,
Assertion Language, Formal Property Language: All used interchangeably
to describe a language that can be used to describe high-level design
specification, properties, events, and assertions. These languages
are designed to provide concise format for complex temporal sequences
and regular expressions.
Assertion Approaches
There are five approaches to assertions that have been described
in the literature.
- Declarative Assertions using a library of
Verilog monitor modules
- Procedural Assertions using a Verilog assert
construct
- Formal property languages
- Pseudo-comment directives
- Post-processing simulation history
As of this writing, various theories about
which methodology is best for assertions are fragmented. The goal
here is not to promote one versus another, but to introduce each
and list some of the commonly documented pros and cons. The examples
used are not meant to be comprehensive but they do cover some of
the more widely discussed methods.
Declarative Assertions
The most common use of assertions today are
the declarative assertions in the Open Verification Library (OVL)
that is freely available at
www.verificationlib.org OVL is an assertion monitor library
of Verilog modules that can be easily instantiated into a design.
OVL provides a consistent way to specify static and temporal assertions
in RTL code. OVL provides a unified message reporting mechanism
that can be easily customized for specific projects by changing
very little code. It also provides an easy way to enable and disable
assertions during simulation. OVL also provides a consistent severity
level scheme that can be used to stop simulation on fatal errors.
Work on OVL is continuing with approximately two new releases per
year. OVL will continue to evolve as related standards stabilize.
OVL is very easy to use and is a good first step to get started
with assertions. It is available now and has been proven and used
on many projects. It's open source format makes it appealing since
it can be customized for each application. Since OVL uses a library
of modules the assertions must be instantiated into the design.
The one capability it does not currently have is procedural assertions
or sometimes called "in-context" assertions.
Procedural Assertions
Instead of instantiating a module from a library
it is at times more convenient to specify assertions using procedural
statements. This is the case with the new assert construct that
is part of the SystemVerilog 3.0 specification approved by Accellera
and work is continuing in SystemVerilog 3.1. Procedural assertions
are useful in the context of a Verilog always block with procedural
code such as a case statement or an if-then-else block. Procedural
assertions can be inserted into the code depending on which branch
has been taken. This allows the assertions to be active during the
context in which they are important. Both declarative and procedural
assertions are good ways to capture design intent during the RTL
coding process. If they are not captured during this phase the knowledge
is probably lost since it is unlikely anybody will go back and insert
these assertions.
Formal Property Language
The next method that has been used for assertions
is the use of a formal property language. These languages are constructed
for the purpose of specifying design properties with minimum effort.
They are very powerful in creating complex temporal expressions
and they also make use of regular expressions to allow complex behavior
to be specified with very little code. These languages have existed
for many years, but have not been used in mainstream design. Current
examples are Sugar that is being used by the Accellera formal verification
committee and the Open Vera Assertions (OVA) used by Synopsys for
formal verification tools as well as in the VCS logic simulator.
The formal property language is useful during all phases of the
project and at all levels of design. System architects can use these
languages to specify high-level properties of the design. They can
be used by verification engineers to perform black-box verification
without understanding all of the details of the design, and by RTL
designers to specify low-level assertions about the code. One of
the points that has been confusing so far about assertions is the
relationship between the formal property language and procedural
assertions such as the SystemVerilog assert language construct.
Certainly, there is much overlap since both can be used to specify
assertions. The formal property language is more general purpose,
not tied to any specific language issues of Verilog or VHDL. Over
time the syntax used to specify properties will converge so that
a single syntax can work for both a formal property language and
HDL language extensions. If this is not possible due to constraints
of the Verilog namespace at least the syntax should be very close.
Currently, tools using a formal property language for assertions
usually put them into a separate file so formal tools and simulators
can process them separately.
Pseudo-Comment Directives
Another approach that has been taken to specify
assertions is the use of pseudo-comments. By embedding assertions
in comments they can be put directly into the RTL code and will
not interfere with the Verilog syntax or require any changes to
the simulator. Formal verification tools can read the comments using
a special parser. In addition to formal methods these tools can
also output a Verilog RTL equivalent for each assertions that allows
the assertions to be simulated and flagged in a standard logic simulator.
This instrumentation process is useful since it can automatically
gather functional coverage metrics about events and assertions during
a simulation run, create a database of activity, and display the
activity in a concise format for users. Data from multiple simulations
can even be merged to form a complete picture of functional coverage.
The methodology is similar to the instrumentation process commonly
used in code coverage. An example of an Axis partner working in
this area is 0-In Design Automation.
Post-Processing Simulation History
So far all of the methods described have done
assertion checking during simulation. A different approach is to
check for assertions after a simulation test is complete. In the
same way engineers use waveform dumps to debug a problem after the
simulation is complete they can check for events and assertions.
An example of an Axis partner working in this area is TransEDA.
They have developed a tool that can read a waveform file in VCD
or FSDB format, read a set of assertions specified in PERL or Sugar,
and provide information about the assertions during the simulation
run. This methodology does not require any changes to the simulator,
any language extensions, or any changes to the design files. Depending
on the number of signals needed and the length of the simulation
it could require large waveform files.
Technology and Goals for
Assertion-Based Methodologies
There is great interest in assertions at Axis Systems since they
are poised to become an important part of every design flow. Axis
is committed to promoting the use of assertions while at the same
time remaining neutral enough to allow our users to choose among
different methods and EDA vendors. Axis is in a good position to
promote all types of assertions and educate engineers on how to
incorporate assertions into a design flow. As a company Axis is
driven by simulation performance. The company's primary value comes
from shortening long simulation times by using our ReConfigurable
Computing (RCC) technology. At the same time Axis places a tremendous
value on simulation productivity by providing advanced debugging
features such as simulation hot swap and VCD-on-Demand that allow
engineers to quickly find problems. Running faster is not enough
if it is difficult to debug and fix problems when they occur. Debugging
inefficiency quickly negates any speed advantage.
The primary goals related to assertions are:
- Enable a consistent methodology between simulation,
acceleration, and emulation
- Map assertion detection into RCC to obtain
highest simulation performance
- Provide the ability to run behavioral code
such as $display and PLI for assertion processing
As designs get larger and larger they will require
some form of acceleration and/or emulation to achieve verification
goals. By enabling faster simulation that works will with assertions
users can leverage both of these emerging technologies to meet project
goals. Historically, the value of emulation was raw performance.
Emulation users have suffered greatly from poor visibility during
emulation. Unlike simulation, emulation does not allow testbench
and monitors to report activity in the emulator. Assertions are
a way to provide this visibility. An efficient implementation of
assertions maintains the performance value of emulation and provides
the visibility to significantly improve emulation debugging. Certainly
running faster is helpful, but if the engineers have to remove the
assertions during emulation this is a major loss of all of the benefits
of assertions already discussed.
Assertion Processor
Assertions can be decomposed into two parts,
detection and failure processing. Assertion detection is done using
state machines. All of the temporal expressions that are used to
write an assertion can be implemented in the form of an RTL state
machine. By definition RCC can run all assertion detection in RCC
hardware at hardware speed. Similar to a microprocessor interrupt,
Assertion Processor receives interrupts when assertions fail and
activates a software service routine that runs on the workstation
and has access to behavioral code such as $display or PLI. Assertion
Processor allows engineers to maintain the use of assertions from
simulation to simulation acceleration and into emulation without
being forced to remove them or execute assertion detection in software
simulation. Assertions become a valuable debugging tool in the historically
difficult to debug emulation environment.
The interrupt driven implementation of Assertion
Processor is more efficient than polling for assertion violations
from a software testbench and does not impact emulation speed when
there are no assertion violations. Polling requires many bits inside
the emulator to be read every clock cycle. If the design contains
10,000 assertions then an equal number of bits must be read every
clock and the bits have to be examined to find out if any assertions
have been triggered and if so then the appropriate assertion processing
code is executed. Testing by Axis has shown polling to be 4 times
slower than an interrupt driven implementation. The interrupt driven
architecture provides the required visibility and the performance
of assertion detection in hardware. The added advance of the RCC
engine is its event-based algorithm. Assertion Processor accurately
handles assertions that are not sampled on clock cycle boundaries
because of the event-based algorithm of RCC. Cycle-based algorithms
and polling on clock cycle boundaries cannot handle these types
of assertions.
For fatal assertions control is required to
stop the simulation instead of wasting simulation cycles. This can
be done from the software service routine using ordinary Verilog
commands such as $finish.
Another feature of Assertion Processor is the
ability to configure it to perform simulation hot swap and stop
during assertion processing. Not only does "swap and stop"
allow behavioral code to be run but gives a user source-level debugging
and full access to all of the signals of the design. Some engineers
prefer to use this interactive style of debugging instead of exiting
the simulation and using post-processing debugging tools. After
debugging is complete the user has the option to exit, continue
to run in the software simulator, or to use simulation hot swap
to load the simulation back into the RCC engine and continue.
As an example of using Assertion Processor consider
the assertion shown in Figure 1. This assertion can be coded using
the assert_change module from OVL as shown in Figure 2. To allow
OVL map to RCC and get the benefits of the $display assertion reporting
the ovl_error task in ovl_task.h is customized. The new code is
shown in Figure 3. When the assertion fails the display_task will
be executed in software on the workstation so the $display is visible
and entered into the simulation log file as usual. A diagram of
how assertion-processing works is shown in Figure 4.
FIGURE 1. Example Assertion
FIGURE 2. OVL Instantiation
FIGURE 3. OVL Modifications
FIGURE 4. Assertion Processor
Execution
Users achieve the highest debugging productivity
by combining Assertion Processor with VCD-on-Demand (VoD) to generate
waveform information. VCD-on-Demand (VoD) alleviates the limitations
associated with large waveform files and the struggle to decide
when to dump and what to dump into waveform files. Users can run
without specifying any dumping and after the run is complete they
can go back and produce a waveform file for any desired window of
simulation time and any scope of the design. Assertions pin-point
design errors and VoD provides the most efficient way to produce
waveforms starting at the point of assertion failure and working
back to the root cause of the problem without re-running simulation.
A diagram of the debugging flow with VoD is shown in Figure 5.
FIGURE 5. Debugging Flow
Axis is currently working with multiple assertion
methodologies to ensure they run well with Axis products, providing
the highest possible performance and debugging efficiency. Details
of specific assertion methodologies and associated design flows
will continue to be documented in white papers and application notes
for users seeking the highest performance verification platform
combined with the latest assertion-based design and verification
techniques.
Summary
Assertion-based verification methodologies are the next breakthrough
in design verification. When this methodology is combined with a
high-performance verification platform, design teams can meet the
challenges of the next generation of complexity. An introduction
to assertions has been provided and the benefits of such methodologies
have been applied to general logic simulation as well as the specific
RCC verification platform from Axis. A methodology has been described
that leverages the emerging set of formal verification tools as
well as the high-performance simulation tools from Axis. Assertion
count in today's ASIC designs typically ranges from 1,000 to 10,000,
and incurs a ten to fifteen percent simulation performance penalty.
With RCC and Assertion Processor assertion detection executes in
parallel with the design and assertions incur no simulation performance
overhead. By accelerating the design and the assertion detection
users get the highest level of simulation performance while maintaining
the increased observability provided by assertions with no change
in design flow. Efficient assertion processing that uses an interrupt
driven implementation also maintains high performance when assertions
fail.
By providing the only general purpose platform
that can accelerate assertions of many types, Axis is leading the
way in promoting the "write-once, run-anywhere" characteristic
of assertions and enabling assertions to be adopted during all phases
of the design cycle. Axis is the technology leader in simulation
productivity with its Assertion Processor, VCD-on-Demand, and simulation
hot swap for advanced simulation control and visibility. Axis is
providing an open system and is working to support emerging assertion
standards and methodologies, and will continue to educate and promote
the use of assertions as standards emerge and methodologies evolve.
For more information about RCC technology visit:
http://www.AxisSystems.com/products
References:
[1] T. Fitzpatrick, H. Foster, E. Marschner,
P. Narain, "Introduction to Accellera's assertion efforts",
EEdesign, June 2, 2002
[2] Synopsys, Inc., "Assertion-Based Verification",
May 2002
[3] H. Foster, "Improving Verification
through Property Specification", D&R Industry Articles
[4] J. Emmitt, "Verifying complex SoCs
with OVL", Electronic Engineering Design, January 28, 2002
[5] 0-In Design Automation, Inc., "Black
& White Assertion-Based Verification Flow", The Verification
Monitor, May 2002
[6] L. Bening, H. Foster, Principles of Verifiable
RTL Design, Kluwer Academic Publishers, 2001
[7] J. Bergeron, Writing Testbenches Functional
Verification of HDL Models, Kluwer Academic Publishers, 2000
|
