Assertion Based Test Generation

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.14, Item 3.0)

From: Tun Lee

I have done some work on automated simulation stimulus generation
based on design's Verilog description to improving the path and
statement coverage.

I found that assertion based verification has got more attention in
functional verification recently. I have download the OVL library and
used it in my design verification projects, and found it very
useful. However, the problem is to violate an assertion, I have to
generate many stimulus. Sometime, even with lots of stimulus, the
assertion will not be violated.

Therefore, I think we can propose a method to generate test data which
will violate the assertions inserted.

My question is are there some existing methods, techniques or
researches for assertion based test generation? Would you be kind
enough give me some advice on this? Thank you!

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.15, Item 7.0)

From: Carl Pixley

Almost all formal verification model checkers (MCs) attempt to do what
Tunlee is asking. If there is a violation of an assertion (i.e.,
property) the MC will report a trace from an initial state to a state
which violates a property. Certainly Synopsys' Magellan does this and
I am sure other model checkers report offending traces as well. Of
course, there is always the issues of (1) capacity of a model checker,
(2) the complexity of the design and (3) the assertion being checked
for violation.

There are many engines which attempt to solve this problem. Any
additional power Tunlee's methods can give us is most welcome.
However, I must caution him that a lot of very good academic and
commercial people have investigated this problem. On the other hand,
having watched automated formal verification methods and algorithms
advance for over a decade, I strongly expect even further advances in
the future.

Tunlee should look at BDD, SAT, ATPG, symbolic simulation and many
other techniques. There is an pretty immense literature on this.

- Carl Pixley, Synopsys

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.15, Item 7.1)

From: Richard C. Ho

The first question that comes to mind is whether doing stimulus test
generation is the best way to achieve verification with
assertions. One of the key features of assertion-based verification is
that the assertions can be operated on with multiple analysis engines,
of which simulation is the basic one. Much more powerful engines
utilizing formal verification can also be used on the assertions.

If you used an _exhaustive_ formal analysis engine, then you could
determine for each assertion whether:
a) a counter-example exists
b) the assertion can be proven true for all time
c) unknown result

The beauty of formal verification is that if you can get result (a) or
(b), then there is no need to use stimulus generation techniques to
drive a simulator through many millions of redundant cycles.

Today's state-of-the-art formal verification engines operate on block
and chip level designs. Refer to www.0-in.com for more details on such
engines. These engines also provide metrics for assertions with result
(c) that can help users determine what further testing is required.

- Richard Ho, 0-in

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.15, Item 7.2)

From: Umberto Rossi

When assertions are introduced in HDL description, it is necessary to
distinguish two cases: (1) triggering the assertions, i.e. making all
of its input signals change, and (2) make the violation occur. Of
course (1) is a pre-condition of (2) and may be considered as a
trivial task, but often checking if all assertion inputs have been
moved, by stimuli generated at top-level, may give some unexpectd
hints.

For the purpose of violating assertions I would use Magellan by
Synopsys. The usage model of this tool includes goalset-based Test
Pattern Generation, where a goalset is a set of internal or output
signals of the circuit. Including in the goalset the assertion's input
and output signals is a good method to stimulate the assertion itself.
Depending on the complexity of the circuit and of the assertion,
Magellan could be able to prove that the assertion can be never
violated, thus excluding the related failure.

- Umberto Rossi, Formal Verification Manager
ST Microelectronics

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.15, Item 7.3)

From: Tarak Parikh

Actually there has been quite some research in the area of automatic
vector generation for designs (See DAC Proceedings for the last 3-5
years). Previously many targets had been explored, such as interesting
states in the state machine, automatic assertions etc.

User written assertions are one of the most appropriate target for
such automated test bench generation. Combining assertions with
constraints to specify legal design space can often lead to finding
the corner case bugs in the easiest possible way.

@Verifier-DCS (Directed constraint solver) from @HDL is one such tool
that combines simulation, formal technology and assertion based
verifi- cation to generate vectors targeted at specific assertions in
the design.

It combines a distributed random constraint solver with a directed
constraint solver to effectively guide the vector generator towards
the user specified assertions . These vectors are optimized to fail
these assertions. These vectors can be then saved to re-verify the
design after design/assertion fix.

Given a design and a set of assertions, formal verification provides
the most complete coverage for the design. Any failure indicates a bug
and a pass indicates that no bug exists for the complete
space. However, given the design size limitations of formal
technology, DCSA provides the most optimal use of assertion based
verification technology.

- Tarak Parikh, @HDL