I want to say:
"if the sequence A occurs then the sequence B occurs within that sequence". How can I do this?
I would have thought I could use the assertion:
assert property (@(posedge clk) (A |-> (B within A));
but this doesn't seem to work for my example.
I've read that:
The linear sequence is said to match along a finite interval of consecutive clock ticks provided the first boolean expression evaluates to true at the first clock tick, the second boolean expression evaluates to true at the second clock tick, and so forth, up to and including the last boolean expression evaluating to true at the last clock tick.
but i suspect that the clock tick passed to the otherside of the |-> the last clock tick when I want it to be the first.
My particular example is an accumulator which I expect to overflow if I add enough positive numbers, so I want A = (input == 1)[*MAX_SIZE] and B = (output == 0), so here B is a sequence of length 1, I don't know if that causes problems.
I'm very new to system-verilog so it maybe that it's some other part of my code which is going wrong but I've not seen this example done anywhere.
You are correct that the consequent in the |-> operator is started once A has already matched. What you want is to look into the past: "once I've seen A, have I seen B within A?".
You could use the triggered property of a sequence to do this:
sequence b_within_a;
@(posedge clk)
B within A;
endsequence
assert property (@(posedge clk) A |-> b_within_a.triggered);
The b_within_a sequence will match exactly at the end of A, of course, if B also happened, which is when the triggered property will evaluate to 1.
Note that the b_within_a sequence has its clock defined specifically. This is a requirement from the LRM, otherwise you won't be allowed to call triggered on it.