Using "not" in SystemVerilog Assertions

SystemVerilog
,
2

In reply to Jung Ik Moon:

  1. The “not” operator is a property operator and is not a sequence operator.
    Thus, the following is incorrect.
    ##1 (not (my_seq), t = t - 1)[*0:$]
  2. If the consequent has a infinite delay range it can never fail; it can succeed
a |-> ##[1:$] b; // same as
a |-> ##1 b or ##2 b or ##3 b or ... ##n b; // can never fail
//
a |->   ##1 (1, t = t - 1)[*0:$] ##1 c; // is same as
a |->  ##1 c or ((1, t = t - 1)[*1] ##1 c) or ((1, t = t - 1)[*2] ##1 c) or ..
// Thus, can never fail
//
a |->   ##1 (b, t = t - 1)[*0:$] ##1 c; // is same as
a |->  ##1 c or ((b, t = t - 1)[*1] ##1 c) or ((b, t = t - 1)[*2] ##1 c) or ..
// This CAN fail because a sequence of " b==1 ##1 b==0" fails the b[*2], and would also fail the b[*3] and etc.
  1. The use of not of a sequence can be confusing. Why not making it a positive type of requirement. Thus instead of [list]
  2. “my_seq to my_seq delay should not be less than my_timing.”, use
  3. “my_seq to my_seq delay should be >= than my_timing.”

[*] You need the **first_match()**operator to get a failure.
[/list]
Below is code, link to the test file, and the simulation results.


int my_timing= 4; 
  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 ) |->  // ** Don't need the "-1", was a copy/paste mistake 
          ##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t);
  endproperty
  ap_my_prop: assert property(my_prop);

seq2seq.sv

1297×613 59.4 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home