Let, Sequence and Property Declarations; Inference - SVA: The Power of Assertions in SystemVerilog - page 171

Let us apply these rules to the example. First consider assertion a_until .For
substituting seq_impl_prop instance body into the assertion requires to determine
its actual arguments. The first two actual arguments are missing in the instance spe-
cification; therefore, default values are used. In this case, they are inferred. For rst
the argument $inferred_disable is inferred from default disable iff and
thus it is !reset .For clk , $inferred_clock is inferred from default clocking
and thus it is posedge clock .
The third argument is an instance of sequence sf_after_a which itself needs
its actual arguments. The first argument is again inferred from default clocking
as posedge clock . The second one is variable w and the third one is an instance
of sequence s . The last argument is for pf , and it is simply x until y where x
and y are variables declared in the module. The assertion with the actual arguments
substituted has the following form:
a: assert property (seq_impl_prop(!reset, ( posedge clock),
sf_after_a(( posedge clock), w, s, 1), (x until y));
We can now proceed with the substitution of the arguments into the body of
seq_impl_prop . It becomes
disable iff (!reset) @( posedge clock)
(sf_after_a(( posedge clock), w, s, 1)) |-> (x until y)
The next step is to substitute the body of the sequence sf_after_a . Its sequence
expression after substitution of the actual arguments becomes
@( posedge clock) w ##1 (v[ * 3])
where (v[ * 3]) is the body of sequence s . The final form of the body of assertion
a_until before clock flow is applied is as follows:
disable iff (!reset) @( posedge clock) (@( posedge clock)
(w ##1 (v[ * 3])) |-> (x until y)
The top-level clock is pushed into the antecedent sequence of the implication and
then flows into the consequent property as explained in detail in Chap. 12 . The result
in this case is a single-clocked property, running on posedge clk .
disable iff (!reset) @( posedge clock)
(w ##1 v[ * 3]) |-> (x until y)
What is the type of expressions x and y ? Since x and y are variables (i.e., Boolean
expressions), these expressions are in fact simple Boolean sequences. They are used
in a property context as the operands of the until operator, hence they are promoted
to properties.
Regarding the cover property statement c_seq , the sequence instance is
identical to one used in the assertion; therefore, the final form of the sequence
expression used in the property expression is as follows:
disable iff (!reset) (@( posedge clock) w ##1 (v[ * 3]))