Writing SVA sequence involving a bus

SystemVerilog
,
12

In reply to pavan yalamanchili:

(my_bus===0) |=> (!($fell(my_bus[i])[->1]) intersect q_all_rose);

  1. !sequence is illegal … in general is it okay to use a “not” operator, like, not(sequence). I know “not” is a property operator and not a sequence operator

From my book, "Guideline : Limit the use of the not property operator in properties where the property_expr is a sequence, Boolean, or property with until, eventually . Do not use the not operator in properties where the property_expr can be vacuous. The reason for this recommendation is that negated assertions that contain the implication operators are difficult to understand and can be misleading. The following property statement specifications demonstrate the issues. The requirements state that a request should never be followed by an acknowledge in the same cycle, thus if req ==1, ack must be ==0 in the same cycle).


not (req |-> ack); // Leads to incorrect results, AVOID THIS structure
req |-> not ack; //  
// Use not for consequent that is a sequence , e.g. (a |-> not(b ##1 c))
req |-> !ack; // Use logical negation for negation of a variable
not(req ##0 ack); //  Does not provide meaningfull coverage
  1. (!$fell[i][->1] is not what you want … I agree… consecutive repetition might have worked

You can use !endpoint_of_a_sequence. You have to think about its use,

can you also comment on these (I have not written the antecedent part of implication operator)


a) (!$fell[i] throughout q_all_rose)) // Not correct code. 
// ** do you mean something like 
 always @ (posedge clk) begin 
        static int i; 
        for(i=0; i <= 31; i++) begin 
          if($rose(my_bus[i])) rose_bus[i]<=1'b1;
          if (flag) ap_fell: assert(!$fell(my_bus[i])); 
          ap_t: assert property(!$fell(my_bus[i]) throughout q_all_rose); //--
        end
    end 
The " ap_t: assert property(!$fell(my_bus[i]) throughout q_all_rose); " causes concurrent assertions in the queue.  That should work. The immediate is a better solution. 
b) (($fell(my_bus[i]) == 0)[*0:$] intersect q_all_rose)
// Same as 
 (($fell(my_bus[i]) == 0)[*0] intersect q_all_rose) or // fail?? 
 (($fell(my_bus[i]) == 0)[*1] intersect q_all_rose)
.. 
 (($fell(my_bus[i]) == 0)[*n] intersect q_all_rose)
// This may work.  You'll need to test it.   Looks complicated.