Resets - SVA: The Power of Assertions in SystemVerilog - page 288

Chapter 13
Resets

The Metropolis should have been aborted long before it became
New York, London or Tokyo.

— John Kenneth Galbraith

As the evaluation of a concurrent assertion evolves over time, certain conditions
may occur upon which it is desired to stop the present evaluation attempt in a
preemptive or abortive way. The prototypical example is the occurrence of design
reset: most concurrent assertions should not continue evaluation across reset of the
design. As a result, such preemptive or abortive conditions have come broadly to
be termed reset conditions . It is cumbersome, at best, to instrument every step
of a concurrent assertion with sensitivity to a reset condition. Therefore, SVA
provides reset constructs with which reset conditions can be declared and their
scopes specified.
This chapter covers declaration, scoping, and semantics of reset constructs. There
are abort property operators which come in both synchronous and asynchronous
forms, and in both passing and failing flavors. These are in addition to the existing
asynchronous disable iff construct at the top-level of a concurrent assertion.

13.1 Overview of Resets

This section gives an intuitive overview of resets based on examples.
A reset condition is a condition upon which it is desired to stop evaluation
of a concurrent assertion or subproperty in a preemptive or abortive way. The
prototypical example is the occurrence of design reset: most concurrent assertions
should not continue evaluation across reset of the design under test. Encoding a
concurrent assertion to be sensitive throughout its evaluation to occurrence of a reset