Here is a spec:
If signal a
is asserted then it must be asserted till signal b
is asserted and then it should de-assert on next clock edge.
I'm reading through 16.9.9 of LRM (as well as http://www.testbench.in/AS_06_SEQUENCES.html) and the way I understood it, above mentioned spec can be written as
property a2b_notA;
@(posedge clk) ($rose (a) ##0 (a throughout b)) |=> (~a);
endproperty
a_a2b_notA: assert property (a2b_notA);
However this fails immediately on second clock edge after starting, and I can't figure out why.
You're correct in wanting to use the
throughout
operator for your assertion, but the code you wrote has some problems. Let's look at it piece by piece.Whenever I write an assertion I pay attention to the natural language description of what I want to check. In your case, we know we want to trigger when
a
goes from0
to1
. Everything that happens afterwards is the behavior that we want to check, so it should be on the right hand side of an implication operator:The way you wrote your assertion, it would only trigger checks if the
throughout
sequence also happened afterrose(a)
. This would cause you to ignore bad behavior.The next piece of the puzzle is "
a
must stay high untilb
is asserted". Here we'll use the throughout operator. The sequence "untilb
is asserted" is expressed asb [->1]
. This is equivalent to!b [*] ##1 b
. Our sequence should thus bea throughout b [->1]
.The
throughout
sequence will end whenb
goes high. At this point we need to check thata
goes low on the next cycle:##1 !a
. I've used logical negation here because I find it clearer than bitwise negation, but the result should be the same.Putting it all together, the whole property should be:
I've used overlapping implication here because
b
could already be high whena
goes high, in which case I'm assuming thata
should go low immediately on the next cycle. If not, you can fiddle with the details yourself.You can find a working example on EDAPlayground.