Using "not" in SystemVerilog Assertions

SystemVerilog
,
7

In reply to Jung Ik Moon:
Your not property would not work either.
If you know that there will be no more than n my_seq, like no more than 10, then you can count the number of valid my_seq and use that count as an antecedent to the rest of the property. Below is the key aspect of this solution:


int my_timing= 4, count_seq;  
    function void inc_count(); 
      count_seq=count_seq+1'b1;
    endfunction : inc_count 
    
    // no more my_seq following.
    property my_prop_nomore;
      int t, count=0;
      @(negedge clk) disable iff (!rstn)
      count_seq <=10 |-> // If >10, then vacuity thereafter
        (my_seq, t = my_timing, inc_count() ) |->  
           ##1 first_match((1, count=count+1'b1)[*0:$] ##1 
                            (my_seq, inc_count())) ##0 (count >= t);
    endproperty
    ap_my_prop_nomore: assert property(my_prop_nomore);

Complete code


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b, rstn=1'b1;  
  int my_timing= 4, count_seq; 
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk;  
    
    function void inc_count(); 
      count_seq=count_seq+1'b1;
    endfunction : inc_count 
    
    sequence my_seq;
      ( a ##1 b); 
    endsequence
    // "my_seq to my_seq delay should not be less than my_timing."
    // "my_seq to my_seq delay should     be >= than my_timing."
    property my_prop;
      int t, count=0;
      @(negedge clk) disable iff (!rstn)
      (my_seq, t = my_timing - 1) |-> 
      ##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t);
    endproperty
    ap_my_prop: assert property(my_prop);  
    // no more my_seq following.
    property my_prop_nomore;
      int t, count=0;
      @(negedge clk) disable iff (!rstn)
      count_seq <=10 |-> 
        (my_seq, t = my_timing, inc_count() ) |->  
           ##1 first_match((1, count=count+1'b1)[*0:$] ##1 
                            (my_seq, inc_count())) ##0 (count >= t);
    endproperty
    ap_my_prop_nomore: assert property(my_prop_nomore);  
    
    initial begin 
      repeat(200) begin 
        @(posedge clk);   
        if (!randomize(a, b)  with 
        { a dist {1'b1:=1, 1'b0:=3};
        b dist {1'b1:=1, 1'b0:=2};
        
      }) `uvm_error("MYERR", "This is a randomize error")
    end 
    $stop; 
  end 
endmodule

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