Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 312

14.5 Event Semantics of Procedural Concurrent Assertions

Before delving into the details of semantics, let us first review event simulation
semantics that are important for the execution of procedural concurrent assertions.
The event semantics of assertion simulation is mostly carried out in three regions:
Active region, Observed region, and Reactive region. Although scheduling evalu-
ation, performing evaluation, and detecting events take place in all three regions,
each region has a unique role in these activities for assertions. The majority of
actual evaluation of assertion expressions takes place in the Observed region, the
scheduling is largely performed in the Active region, and the Reactive region is used
for processing the action blocks. The role of the regions and their order is depicted
in Fig. 3.2 .
To support procedural concurrent assertion evaluation within the event simu-
lation semantics, two new semantic objects are introduced: procedural assertion
queue and matured assertion queue .
A procedural assertion queue is used as a temporary holding place for instances
of assertions that have been invoked, together with any captured values of variables.
These assertion instances pend in the procedural assertion queue until it is deter-
mined in the Observed region that they should mature for evaluation. Thereupon,
the assertions are transferred to the matured assertion queue to await the arrival of
their respective leading clocks. Each procedure, such as always or initial , that
contains procedural concurrent assertions has its own procedural assertion queue.
There is only one matured assertion queue for all procedures. While in a procedural
assertion queue, prior to maturing, an instance of an assertion can get purged, as we
will illustrate later in the examples.
Note that these semantic objects have no explicit representation in the language.
Their sole purpose is to explain the semantics of procedural concurrent assertions.
Here are the roles of the two queues for processing an assertion:

1. In the Active region, when procedural execution reaches a concurrent assertion,
an instance of the assertion is entered in the procedural assertion queue of the
process, together with any captured values of variables for that instance.
2. During the execution in the Active region, an assertion instance waiting in the
procedural assertion queue may get purged.
3. In the Observed region, all surviving assertion instances from the procedural
assertion queues mature and are transferred to the matured assertion queue.
4. If the leading clock of a matured assertion instance did trigger in the Active
region, then the evaluation attempt of that assertion begins and the assertion
instance is removed from the matured assertion queue to follow its normal course
of evaluation. Otherwise, the assertion instance waits in the matured assertion
queue until its leading clock triggers in some future time step.