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

the sequence instance will be inferred from the instantiation context (see Chap. 14 ),
and the formal argument s will be replaced by x . This variable or sequence definition
x must have been declared in the scope of the declaration of s_def .
Next, we discuss property declaration, in particular in its differences from a
sequence declaration.

8.2.2 Syntax of Property-Endproperty

The syntax of a property declaration is quite similar to that of a sequence
declaration. The differences are as follows:

1. The encapsulation keywords are property - endproperty .
2. The formal and actual arguments can also be property expressions . The type of a
formal argument may thus be property .
3. The body of a property declaration may contain property operators and refer
to other property instances .
4. Local variable argument can only be local input (see Chap. 16 ).
5. The property may contain disable iff (condition) definition. The default
actual argument to a formal of some integral type (or untyped) can be

$inferred_disable (see Sect. 8.3 ).
The first one is obvious. The second and third differences are a natural extension
from sequences to properties in that a property can receive a property expression
as its argument and can operate on properties. Note also that under the property
expression, sequence expressions and integral expressions are type compatible
actual arguments. The fourth difference is because local variables do not flow out
of properties (see Chap. 16 ). In properties, local variables have nowhere to flow out
since no concatenation of properties exists. The fifth difference provides means to
pass a default disable expression to a top-level property instance in an assertion.
Some of these points are illustrated in the next example:

Example 8.13.
module m;
bit clock, reset, a, b, c, d;
default clocking @( posedge clock); endclocking
...
property p1( bit rst, event clk = $inferred_clock, untyped x,
property p);
disable iff (rst) @clk !x ##1 x |-> p;
endproperty

property p2;
a |-> (b until c);
endproperty

a_imply: assert property (p1(.rst(reset), .x(d), .p(p2)));
...
endmodule