I am trying to write an assertion, the spec goes like: if a is high in any cycle, then for the next 3 cycles, c should be assert if b is not asserted. If anytime b is asserted, c should be deasserted in the next cycle.
I tried below but not sure how to add b in this scenario.
a |-> c[*3]
Should I just disable the assertion when b is asserted? Thanks for help.
if a is high in any cycle, then for the next 3 cycles, c should be assert if b is not asserted
Try this sequence:
a |-> (c [*3] && !B [*3])
If anytime b is asserted, c should be deasserted in the next cycle.
Try adding this other sequence:
b |-> !c
It will check b at the clocking event you describe in the sequence or a defaulting clock, I believe.
Draw a waveform of the assertions of these sequences and check whether they provide what you need or not.
If you want to see the combined behavior of these two assertions, to check for conflicts for example, you can make a third sequence by anding them and checking the waveform.
I am not sure I am fully clear on the spec but goes something along the lines of :
a |-> ##1 (c && !b)[*3] or (b[->1] ##1 $fell(c))
Now this in itself does not make much sense as the second seq for b being asserted and negedge on c does not have an end point. If the spec is for all of this to happen within 3 cycles:
sequence option1; (c && !b)[*3]; endsequence
sequence option2; (b[->1] ##1 $fell(c)); endsequence
a |-> ##1 ((option1 or option2) throughout ##3 1);
Note a few things: - the extra cycle as your spec said for the next 3 cycles. My interpretation of the spec could be wrong here - I coded the two options in two separate sequence to emphasize the point. As long as either one holds, your prop will hold. - This is a literal transcription of your spec (or my interpretation of it). If you actually work out all legal options you can probably simplify the property as a single sequence though it will likely impact readability wrt specification
