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

1 sequence s_start_and_complete;
2

tagType tag;

(start, tag = tagIn)

3

##1 (

4

!(start && tagIn == tag)

5

throughout

6

(complete && tagOut == tag)[->1]

7

8 );
9 endsequence
10 property p_start_and_data_checks;
11 dataType data;
12 (start, data = dataIn)
13 |->
14 s_start_and_complete
15 ##0 dataOut == data;
16 endproperty
17 a_start_and_data_checks: assert property (
18

p_start_and_data_checks

19 );
20 a_complete_check: assert property (
21

complete |-> s_start_and_complete.triggered

22 );

Fig. 15.17 Encoding of all tag protocol checks using only local variables

of sequential code between the auxiliary sequence and the correctness property
p_start_and_data_checks , the latter has been reorganized to instantiate the
former in Line 14 as part of the consequent of the operator |-> . The result is
equivalent to the version of the property in the previous encoding. Sequence method
triggered is applied to the instance of the auxiliary sequence in Line 21 .This
method converts the sequence instance into a Boolean that is true in any cycle
in which the sequence finishes a match and is false otherwise, accomplishing the
communication of the announcement.
Because there are two instances of the auxiliary sequence, this solution incurs a
nominal doubling of the local variable storage for tags as compared to the previous
encoding. A tool could mitigate or eliminate this storage overhead by recognizing
that the antecedent start of |-> in Line 12 is not restrictive on the possible matches
of s_start_and_complete in the consequent.

Exercises

15.1. Show that if the three assertions of Fig. 15.3 hold, then the following assertion
also holds:

a_mutex: assert property (!(start && complete));