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

before any typed ports is stated on the port list. How is the type determined, used,
and verified in that case? For example, consider the following sequence interface:
sequence s_def(a, event b, int c, d, untyped s);
The port a is untyped and its type correctness depends on where it is used in the
sequence. Port b must be a clocking event expression. Ports c and d are of type two-
valued integer. The actual arguments bound to these ports must be type compatible
with int . Finally, since s is preceded by untyped , the actual argument bound to this
port can be anything compatible with its use in the sequence expression. Suppose
that the sequence expression is as follows:
@ba&&(c==d)##1s
In this case, a is restricted to be an integral expression, and c and d can be any
integral type that can be cast to int . The actual argument bound to the last port, s ,
can be an expression or a sequence expression including a sequence instance. This
is because it is used alone as one of the operands of the sequence operator ##1 .Ifit
were used as a in an expression, its type would have been restricted the same way
as for a .
Consider now a different sequence expression:
@b (a + c == d) ##1 s
Let v be a variable of type bit , and the actual arguments of s_def be 2'b11 + v ,
( posedge clk) , 1 , 0 , v . When the actual arguments are substituted to the sequence
expression, we obtain
@( posedge clk) ((2'b11 + v)+1==0)##1v
Suppose that v is 1'b1 over two clock cycles. Will the sequence match or
not? Before substituting the expression 2'b11 + v for the formal argument, it is
enclosed in parentheses and cast to its self-determined type. Therefore, the result
is an unsigned two-bit expression. When the value of v is 1'b1 ,itis 0 extended
to 2'b01 before being added to 2'b11 . The addition yields the result 2'b00 .This
result is then sign extended to int which yields 0+1==0 as the final Boolean
expression. The sequence thus does not match at the first clock tick. If v were 1'b0
in the first clock cycle and 1'b1 in the second clock cycle, then the result of the
addition is 2'b11 , which after sign extension to int yields -1 . Therefore, the result
of the addition with 1 is 0 . Consequently, the first expression evaluates to true, and
the sequence will match at the second clock tick since v is 1'b1 .
Actual arguments to sequences are enclosed in parentheses and cast to
their self-determined type before being substituted for occurrences of formal
arguments in the sequence body. The same applies to actual arguments to
property instances discussed in the next section.