Stable pwrite until pready

SystemVerilog
1

I was curious to understand this semantic here I’ve seen in a public repo:

The requirement:

pwrite remains stable (unchanged) throughout the entire wait state period of an APB transaction — from when penable rises until pready asserts.

The property:

property p_stable_pwrite;
  disable iff(!presetn) 
  $rose(penable) ##0 !pready[1:$] |-> $stable(pwrite);
endproperty

Can we say the antecedent is a multicycle sequence that lasts from when penable raises and pready remains low? I have hard time picturing it.

IMHO the antecedent is not a multicycle of the usage of $rose which will not be true on the second cycle and therefore the behavior of pwrite will only be checked for the first cycle.

A more appropriate check would rather be something along these lines:

property p_stable_pwrite;
  disable iff(!presetn) 
  $rose(penable) |-> $stable(pwrite) throughout pready[->1];
endproperty

Thanks for your comments

EDIT: additional analysis and a proposed alternative

2

This check makes sense when pready signal is low at the clock edge that $rose(penable) is true

( as pready could be asserted at same clock or before $rose(penable) is true )

As per APB protocol : PWrite and PAddr are driven along with PSel’s assertion ( and penable is asserted at the next clock of Psel )

I would write the concurrent assertion as


property p_stable_pwrite;
  disable iff(!presetn) 
  $rose(penable) ##0 !pready |-> $stable(pwrite) throughout pready[->1];
endproperty
3

This check makes sense when pready signal is low at the clock edge that $rose(penable) is true

( as pready could be asserted at same clock or before $rose(penable) is true )

Uhm… interesting observation. Indeed a completer that is always ready could decide to fix the pready to 1. In that case the completion of the transaction would be determined by penable itself.

I guess that checking pwrite or paddr stability would only make sense when the completer uses pready to slow-down the access, i.e. introduce a wait-state.

4

A few comments regarding your 1st property

(1) It should be !pready[*1:$] ( Note that * is missing in your code )

(2) Once $rose(penable)is true for an attempt it isn’t sampled again.

It’s the !pready[*1:$] that makes the antecedent multi-threaded ( Google multi-threaded antecedent you will find a few papers on it )

(3) The property has a limitation.

On the clock that handshake occurs ( assuming there are wait states ), it doesn’t check for $stable(pwrite) i.e whether pwrite is stable on the clock that pready is asserted.

Ideally pwrite should be stable on the clock edge that handshake occurs and there should be a check for it

5

you are right, I failed to understand that a range operator was leading to a multi-threaded antecedent. The catch in my thinking was that with $rose(penable) only one thread was created, as any following cycle would have that boolean false. But after carefully reviewing how the property engine works, in reality the above antecedent is equivalent to say:

($rose(penable) ##0 !pready) |-> $stable(pwrite)) and
($rose(penable) ##1 !pready) |-> $stable(pwrite)) and
($rose(penable) ##2 !pready) |-> $stable(pwrite)) and
($rose(penable) ##3 !pready) ...

So a new attempt is made for every possible delay between penable and pready. When pready is then finally asserted it would make the assertion vacuous. So now all threads must succeed, as the consequent is going to be evaluated for all of the possible delays.

Using throughout I believe that is covering that. The operator will make the check on pwrite stability up until pready is asserted, including the last cycle.