Check that a sequence does not occur within other sequence

Hi, how can I build a sequence that it is true, only when another sequence has not happened. Let me put an example if I have this sequence:


      |------/-/------|---------/-/---------|
      A               B                     C
    (trigger)       (seq1)                (seq2)

How can I impose that between B and C there isn’t another B in between ?


sequence s_no_set_at_dst(set, set_dst, dst);
    ##[0:$] set ##0 set_dst != dst;
endsequence

sequence s_no_clr_at_dst(clr, clr_dst, dst);
    ##[0:$] clr ##0 clr_dst != dst;
endsequence

sequence s_no_set_within_rd(set, set_dst, re, re_dst, dst);
    @(posedge clk_i) s_no_set_at_dst(set, set_dst, dst) within ##[0:$] (re ##0 re_dst == dst);
endsequence 

sequence s_no_clr_within_rd(clr, clr_dst, re, re_dst, dst);
    @(posedge clk_i) s_no_clr_at_dst(clr, clr_dst, dst) within ##[0:$] (re ##0 re_dst == dst);
endsequence

property p_clr_set0_rd (clr, clr_dst, set, set_dst, re, re_dst, out);
    logic [5:0] _dst;
    @(posedge clk_i) (clr, _dst = clr_dst) |-> 
        ##[1:$] (set ##0 set_dst == _dst) 
        ##[1:$] ((re ##0 re_dst == _dst) and s_no_clr_within_rd(clr, clr_dst, re, re_dst, _dst) and s_set_within_rd(set, set_dst, re, re_dst, _dst))
        ##2 out == 1'b0;
endproperty 

This is the code I have. Which is trying to detect if s_no_set_at_dst or s_no_clr_at_dst occurs while this sequence ##[0:$] (re ##0 re_dst == dst) is “waiting” to happen. But is not working.

Thanks

In reply to Sustrak:

How can I impose that between B and C there isn’t another B in between ?
[Ben] I would use the “not” property operator.

 start_seq |->
  not(##[1:*] Bseq  ##[1:*] Bseq) and
  ##[1:*] Bseq ##[1:*] Cseq;

I didn’t look at your specific code.
This code may never finish because of the ##[1:*].
It would be best if this is constraint, like ##[1:50]
Ben systemverilog.us

In reply to ben@SystemVerilog.us:

Right, but it seems that you can not do not seq to negate a sequence. Instead you have to write the sequence already negated.

That was the problem I was facing, with the negated sequence, the code I put above works fine.

Salut!

In reply to Sustrak:

you can not do not seq to negate a sequence.

You are correct that you cannot do a logical “not” of a sequence (i.e., !(a_sequence).
However, the not operator is a property operator, and my operations are on properties. When I write

 
start_seq |->
  not(##[1:*] Bseq  ##[1:*] Bseq) and
  ##[1:*] Bseq ##[1:*] Cseq;

// I am writing 
  A_sequence  |-> not(A_property) and (a_property)
// A sequence can be a property 
property_expr ::=
  sequence_expr
| not property_expr
| property_expr or property_expr
| property_expr and property_expr
| sequence_expr |-> property_expr
// Thus, the following is legal 
  A_sequence  |-> not(A2_sequence) and (A3_sequence)

Below is a testbench, also at http://SystemVerilog/vf/abnotb.sv

Images of results


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b, c, d;  
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk; 
    // not(##[1:*] Bseq  ##[1:*] Bseq) and   ##[1:*] Bseq ##[1:*] Cseq; 
    
    ap_not: assert property(@ (posedge clk) 
       $rose(a) |-> (not(##1 b ##[1:2]c ##1 b ##[1:2]c))  and 
                        (##1 b ##[1:2]c                  ##1 d)); 
     
    ap_B: assert property(@ (posedge clk) 
                        $rose(a) |-> // (not(##1 b ##[1:2]c ##1 b ##[1:2]c))  and 
                                         (##1 b ##[1:2]c                  ##1 d)); 
    
    ap_notB: assert property(@ (posedge clk) 
                        $rose(a) |-> (not(##1 b ##[1:2]c ##1 b ##[1:2]c))); 
 initial begin 
     repeat(200) begin 
       @(posedge clk); ##1;  
       if (!randomize(a, b, c, d)  with 
           { a dist {1'b1:=1, 1'b0:=4};
             b dist {1'b1:=2, 1'b0:=1};
             c dist {1'b1:=10, 1'b0:=1};
             d dist {1'b1:=5, 1'b0:=1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  

 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment