How to write assertion for eventually (!outstanding) but only if a given flag stays asserted

SystemVerilog
,
1

I have a set of assertions and assumptions where I want to assert something like:
assert (s_eventually !outstanding);
But I also use a flag internally to identify some specific state, so really what I want is this:
IF flag is always true then s_eventually !outstanding
But if flag goes false - no failure

Hoping for something like:
assert ((always (valid)) |-> s_eventually (outstanding == 0));
But this isn’t legal.

Seems like the assertion would trivially pass by the flag going false. Is there any way around this?

Thanks

2

In reply to nachumk:
use the impies property operator where both antecedent and consequent start at the same time/ Also, see Reflections on Users’ Experiences with SVA, part 2

Addresses the usage of these four relationship operators: throughout, until, intersect, implies


bit  clk,  valid, outstanding;
  assert property (@(posedge clk) always (valid) implies 
             s_eventually (outstanding == 0));

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh