Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 69

Assertions can be viewed as an observer machine that produces pass/fail output.
This would be the case when assertions are included as part of the design in
emulation or in formal verification (see Chap. 21 ). In simulation, however, a
different view can be taken that is more suited for understanding the assertion
behavior and debugging. In this view, an assertion is considered as a machine that
issues an evaluation attempt or transaction at every tick of the leading clock of
the assertion (while it is enabled) and ends by its success or failure. Each such
transaction thus has a certain duration in time and can be controlled and analyzed
separately from other such evaluation attempts. This chapter discusses this attempt-
based view of assertion evaluation in simulation and examines efficiency issues
connected with this view.

4.4.1 Simulation Evaluation Attempt

To explain the notion of a simulation attempt, let us consider the following assertion:
a1: assert property (@( posedge clk)a ##1 b);
In this case the assertion has only a single clock that determines the instants at
which the assertion evaluation progresses. This is also the so called leading clock of
the assertion. When later we discuss assertions that refer to multiple clocks, the one
clock among them that starts the evaluation attempts (there can be only one such
clock in SystemVerilog Assertions) is also referred to as the leading clock.
The clocking event is the rising edge of clk which is also the assertion leading
clock. In simulation, the assertion will observe the values of signals a and b starting
at every tick of posedge clk . Thus, at clock tick t the evaluation of a is performed,
and if the result is true, it is followed by the evaluation of b at the next tick, t C 1.If
either a==0 at t or b==0 is true at t C 1, the evaluation starting at t fails at time t or
time t C 1, respectively. However, if both a==1 at t and b==1 at t C 1 are true, then
the evaluation that started at t succeeds at t C 1. An evaluation starting at clock tick
t is independent of the evaluations starting at all other clock ticks. Consequently,
the evaluation result of the attempt at t is independent of the results of attempts at
all other clock ticks, and is thus called an evaluation attempt (starting at tick t ).
Each such attempt has a start time corresponding to the simulation time of the
leading clock tick, and an end time corresponding to the time of the clock tick at
which the evaluation attempt either succeeds or fails. Furthermore, several attempts
starting at different times may be under evaluation at the same time in a sort of
pipeline fashion. For instance in our simple example, if a and b were true for several
clock ticks, there would be two concurrent attempts. If the sequence definition
spanned more than two cycles, more than two attempts could independently be
evaluated at the same time.