Property operator in sequence context #SVA

SystemVerilog
, ,
1

Hi,
Following property shows elab issue: Property operator usage is not allowed in sequence context.
What is wrong with it? How should it be written to resolve elab issue?

(sig1==0) |-> ##7 (($stable(sig2)) until (sig1 [->1]));

When I replace “until” with “throughout” it doesn’t show any issue.

2

In reply to abhiraj171:

The issue you’re encountering is related to the use of the “until” operator within the sequence context in SystemVerilog assertions. The “until” operator is not allowed directly in a sequence. However, the “throughout” operator can be used in a sequence context.

When using the “until” operator, it is typically used in a property or an assertion outside of a sequence. If you need to express a similar condition within a sequence, you might need to reformulate it using other temporal operators.

Here’s an example that captures the essence of your original property using “throughout”:


property property_name;
  (sig1 == 0) |-> ##7 (sig1 throughout [->1] (sig2 == 1));
endproperty

your_sequence : sequence;
  // Sequence body
  // ...
  assert (property_name);
endsequence

In this example, I’ve replaced the “until” operator with “throughout,” which is allowed within a sequence context. This sequence asserts that when sig1 is 0, then for the next 7 time units, sig2 remains stable (does not change) until sig1 changes.

If the specific behavior you are trying to capture requires the “until” operator, you may need to express it in a property outside of a sequence or adjust the formulation to use other temporal operators that are allowed within a sequence context.

3

In reply to ThangDH2405:

Please stop posting unverified code from chatGPT.

4

In reply to dave_59:

Hi Dave,
What would be the correct solution?

Thanks!

5

In reply to abhiraj171:

The issue is that until operator is a property_expression and a property_expression can’t be written as LHS/RHS of delay ‘##’.

property_expression in your code is (($stable(sig2)) until (sig1 [->1]))

What is the intent of using delay ##7 in consequent ?

6

In reply to MICRO_91:

The intent is to check after 7 clk cycles.

7

In reply to abhiraj171:

Try


  property ab;
    @(posedge clk) (sig1==0) ##7 1 |-> (($stable(sig2)) until (sig1 [->1]));
  endproperty