An Apology for Local Variables - SVA: The Power of Assertions in SystemVerilog - page 348

if it exists, announces itself. The medium of communication is the static bit
complete_justified .
The communication mechanism works as follows. In every time step in which
posedge clk occurs, the communication bit is cleared by writing the value 1'b0
into complete_justified in Line 3 . This assignment does not change the sampled
value of complete_justified in that time step. If complete occurs and there is
a thread of evaluation with tag == tagOut , then that thread will finish match of
Lines 14 - 16 and execution will proceed to Line 18 , where t_justify_complete
is called. Line 18 illustrates attachment of a subroutine call to a sequence. The
sequence in this case is just the Boolean 1'b1 . Like local variable assignments,
subroutine calls may appear in such a comma-separated list, and they are scheduled
to execute in the Reactive region in the order that they appear. When it executes,
the task t_justify_complete advances to negedge clk (Line 5 ) and then writes
the value 1'b1 into complete_justified (Line 6 ). The value 1'b1 will remain in
complete_justified until after the Preponed region of the next time step in which
posedge clk occurs. Thus, a thread announces itself as justifying a complete by
causing the sampled value of complete_justified to be 1'b1 in the time step of
the next occurrence of posedge clk . Later in that time step, the value 1'b0 will
again be written into complete_justified by Line 3 , clearing the communication
bit.
The assertion a_complete_check simply looks for an announcement by
requiring that complete_justified be high the cycle after each occurrence of
complete . Because the reference to complete_justified in Line 25 uses the
sampled value, it is able to see the announcement even though the communication
bit is also cleared in the same cycle. This accomplishes the validation of complete
as specified in Rule 5 of the tag protocol.
This encoding shows management of complete_justified by clearing it at
posedge clk (Line 3 ) and setting it at negedge clk (Line 5 ). Other schemes will
work provided the value 1'b1 set in task t_justify_complete persists to the
Preponed region of the time step of the next occurrence of posedge clk .

15.6.2 Tag Protocol Using Only Local Variables

In the previous solution, the mechanism for announcing the existence of a justifying
thread relies somewhat delicately on the SystemVerilog scheduling semantics in the
way the static bit complete_justified is updated. Another approach is to code
an auxiliary sequence that will match exactly when a justifying thread exists and
finishes matching Lines 14 - 16 of Fig. 15.16 . The existence of a justifying thread
is then detected by reference to the endpoint of match of this sequence using the
sequence method triggered (see Sect. 11.2.1 ). No auxiliary static bit is needed.
Such an encoding is shown in Fig. 15.17 .
The auxiliary sequence is s_start_and_complete . It simply mimics the tem-
poral patterns of Lines 11 - 18 of Fig. 15.16 . In order to maximize the sharing