In reply to ben@SystemVerilog.us:
Hi Ben,
Yes, I’m doing formal verification, not simulation.
In the design, tag will only vary from 1-7, but as you said, the formal tool may extend this to 15 assertions. Not sure how do they define vacuity, if all 15 antecedents have to be satisfied, then this can explain the behavior we saw becauwe 8-15 will never be triggered in RTL.
Sure, if I get any further feedback from them, I will let you know. Really glad to have this opportunity to discuss with you and learn from you:)