In reply to ben@SystemVerilog.us:
Sorry Ben. I don’t get what you are saying. The assume directive says to formal that the inputs are constrained. It says nothing about the design cannot be satisfied with the constraint. The counter example shows an input sequence that I have constrained so that it doesn’t happen. The assertion failure is relative to the outputs doing something that I do not expect but the case is not valid because of the illegal input sequence.