How can I use SystemVerilog sequence properties in asserts?

Question

I want to say "if there are an unlimited number of inputs, eventually I get an output", how can I do this?

In other parts of the script I want to assume a limited supply of inputs so I can't just write "assume there are an unlimited number of inputs" and have that hold globally.

So far I've written properties:

property always_another_valid_input;
   @(posedge clock) ##[1:$] valid_input;
endproperty

property foo;
    @(posedge clock) always_another_valid_input |-> ##[0:$] bar == 1;
endproperty

assert property (foo);

but when I run this I get an error: property instance always_another_valid_input is not allowed in sequence expression.

If I replace either side of the |-> with a non-sequence property then I still get an error. It only works when both sides are non-sequence properties.

Is there a good way to work around this?

Answer 1

Refer to IEEE Std 1800-2012 § 16.12 Declaring properties, and more specifically § 16.12.6 Implication, you will see the |-> syntax ussage is described as:

property_expr ::=
    ...
    sequence_expr |-> property_expr
    sequence_expr |=> property_expr

The left hand side must be a sequence or sequence expression. It cannot be a property even if that property only contains a sequence expression.

If you declare always_another_valid_input as a sequence instead of a property, your code will compile

sequence always_another_valid_input;
   @(posedge clock) ##[1:$] valid_input;
endsequence