Assertion does not fail!

SystemVerilog
,
3

In reply to dave_59:

Thanks much, Dave. Your first solution actually does exactly what I want. The only difference is that my spec expected the entire sequence to start with $rose(tagError). But checking for level sensitive tagError will work. I should have thought of moving part of the expression as an antecedent.

Your second solution has a typo (mCheck is repeated twice). Should be,

property p1;
@(posedge clk)
tagError && ($rose(tErrorBit) | $rose(mCheck)) |-> $rose(mCheck) && $rose(tErrorBit);
endproperty

Thanks again.