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
