How to use throughout operator in systemverilog assertions

Question

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.

Answer 1

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 from 0 to 1. 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:

$rose(a) |-> ... something ...

The way you wrote your assertion, it would only trigger checks if the throughout sequence also happened after rose(a). This would cause you to ignore bad behavior.

The next piece of the puzzle is "a must stay high until b is asserted". Here we'll use the throughout operator. The sequence "until b is asserted" is expressed as b [->1]. This is equivalent to !b [*] ##1 b. Our sequence should thus be a throughout b [->1].

The throughout sequence will end when b goes high. At this point we need to check that a 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:

$rose(a) |-> (a throughout b [->1]) ##1 !a;

I've used overlapping implication here because b could already be high when a goes high, in which case I'm assuming that a 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.