Jump to content

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


Recommended Posts

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
sequence seqB;
  B[->1];                  //B high for 1 cycle
sequence seqC;
  (1[*10]);                //10 clk cylces

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[*]);
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 

Link to comment
Share on other sites

Join the conversation

You can post now and register later. If you have an account, sign in now to post with your account.
Note: Your post will require moderator approval before it will be visible.

Reply to this topic...

×   Pasted as rich text.   Paste as plain text instead

  Only 75 emoji are allowed.

×   Your link has been automatically embedded.   Display as a link instead

×   Your previous content has been restored.   Clear editor

×   You cannot paste images directly. Upload or insert images from URL.

  • Create New...