User guide

23-18
SystemVerilog Assertion Constructs
The last property is invalid because it instantiates a sequence with a
different clock tick than the clock tick for the property. In the valid
properties you see the following:
How to specify the clock tick in the property for the sequence it
instantiates.
How to specify a clock tick both in the property and in the sequence
instantiated in the property, if they specify the same clock tick.
That instead of instantiating a sequence you can include a
sequential expression like
sig1 ##1 sig2.
You can declare a property in the following places in your code:
In a module definition
In an interface definition
•At $root (in SystemVerilog $root means outside of any other
definition, a property defined in $root is globally accessible).
Note:
The SystemVerilog LRM says that you can declare a property in
a module definition but never in an always or initial block.
Using Formal Arguments in a Property
Like sequences, you can include formal arguments in properties.
Unlike sequences you cannot use or instantiate a property in another
property. You use or instantiate a property in a concurrent assertion.
For example:
property p3 (sig1,sig2);
@(posedge clk2) sig1 ##1 sig2;
endproperty