SeqA |-> SeqA may not happen again before the first of SeqB or SeqC

[ljepson74]

How can I write the following sequence?

If sequence A happens, then sequence A may not happen again until either sequence B or sequence C happens.

An example of the sequences might be:

sequence seqA;
  ($rose(A)) ##1 $fell(A); //single cycle A pulse
endsequence
sequence seqB;
  B[->1];                  //B high for 1 cycle
endsequence
sequence seqC;
  (1[*10]);                //10 clk cylces
endsequence

 
It is important in this question that seqA is a sequence, so that we are not just checking 
seqA |-> (!A throughout (seqB or seqC))
(For this simple example, after seqA, perhaps a 2 cycle pulse of A is acceptable, before seqB or seqC.  So we specifically check for a 1 cycle pulse of A.)

Although some auxiliary/extra code outside of the sequences and property (perhaps a small state machine) might help, I attempt to avoid extra code, to better understand SVA.

One of my many failed attempts involves something like a liveness property.  Is this a correct/possible approach?

sequence seqA_with_buffer;
  (##[0:$] seqA ##1 1[*]);
endsequence
seqA |-> ( (not seqA_with_buffer) ##0 seqB ##0 seqC )      

//edit: Now that I look at this again (after posting), I don't think the buffer is needed ... if this could be made to work

Some non-working code is here: https://edaplayground.com/x/5z5n