Unexpected SVA failure using s_until_with

SystemVerilog
,
1

Hi,
I was trying a SVA for following requirement:

“Once a ‘read’ has been issued, another ‘read’ for the same readID cannot be re-issued until a readAck with the same ID has returned”

One of the solution I coded was using s_until_with: edalink

For the stimulus I observe that assertion fails once at T:85 ( as per expectation ).
However, there is a 2nd failure at T:89 , which I am not clear with.

I understand if simulation completes and strong operator is in effect, the assertion would fail if the sequence_expr (within the strong operator)isn’t true.
In my case although the antecedent is true for 2nd time at T:85 , the consequent hasn’t began evaluation yet ( due to |=> ) ,
so my expectation is that there shouldn’t be a 2nd failure at T:89.

Any thoughts/suggestions ?

2

In reply to Have_A_Doubt:
Unexpected failure using s_until_with(1) - EDA Playground // code
EPWave Waveform Viewer // wave
I don’t see a 2nd failure

3

In reply to ben@SystemVerilog.us:

Hi Ben,
Although the flag ‘fail’ in the dump is seen as 1, the output log using Questa shows:
**# Assertion fails at T: 85

** Note: $finish : testbench.sv(47)

Time: 129 ns Iteration: 0 Instance: /tb

Assertion fails at T:129**

EDIT: In my code simulation ends at T:89. The output log on Questa shows:
**# Assertion fails at T: 85

** Note: $finish : testbench.sv(43)

Time: 89 ns Iteration: 0 Instance: /tb

Assertion fails at T: 89**

4

In reply to Have_A_Doubt:

(time 129 NS) Assertion tb.ap_proper has failed (5 cycles, starting 85 NS) because at
t85 you have a new successful attempt with ($rose(read), localID = readID)
The consequent suntil_with(localID) was not true before the end of sim.
You have an s_until

5

In reply to ben@SystemVerilog.us:

Ben,
There is a difference in the 2 codes, in my example the simulation ends at T:89.
In my case ( edalink ) ::
Although the antecedent is true at T:85 for 2nd $rose(read), the consequent doesn’t began evaluation till T:95 ( due to |=> ).
This means the strong operator isn’t in effect , so why does assertion fail for 2nd time at T:89 ( when simulation ends ) ?

The 1st failure at T:85 is expected whereas the 2nd one at T:89 isn’t.

In your code ::
The 2nd error is as per expectation due to strong operator being in effect from T:95.
Yet I observe fail == 1 and not fail == 2 during end of simulation at T:129, why is it so ?

6

In reply to Have_A_Doubt:

In your code ::
The 2nd error is as per expectation due to strong operator being in effect from T:95.
Yet I observe fail == 1 and not fail == 2 during end of simulation at T:129, why is it so ?

The assertion did not complete with a failure, thus the action block was not exercised.
The notification of failure was issued by the tool because it was an incomplete assertion of a strong property.

Ben

7

In reply to ben@SystemVerilog.us:

The assertion did not complete with a failure, thus the action block was not exercised.
The notification of failure was issued by the tool because it was an incomplete assertion of a strong property.

Got it.

Would like to hear your comments on whether the assertion failure is as per expected at time:89 ? ( in my example )