Search the Community
Showing results for tags 'negation'.
Found 1 result
-
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
