Using "not" in SystemVerilog Assertions

SystemVerilog
,
5

In reply to Jung Ik Moon:

In reply to ben@SystemVerilog.us:
Some more questions on your answer.

  1. By modifying “should not be < than” to “should be >= than”, isn’t it more likely to become an incomplete assertion at the end of the simulation?
  2. How should I interpret incomplete assertions in this case? Can I just say it PASSED?

An assertion can be in one of the following states:

  • vacuous
  • pass or success
  • fail
  • in execution;
  • Incomplete if the simulation ends and the assertion has not succeeded or failed.
    An incomplete assertion will be identified as FAIL if the sequence is marked as strong.

Assertions are written to express requirements. I don’t see a difference in expressing that a delay should not be less than or equal to5 cycles and delay should be greater or equal to 5 cycles. Where is the INCOMPLETION? An assertion is incomplete if you have not provided enough cycles in the simulation to complete.

[*] Is is possible to write a property sticking to “should not be < than”? This is just to solve the incompleteness issue, IF needed.

  • i.e., “when my_seq is issued, my_seq cannot be issued within my_timing.”

[/list]


 property my_prop;
    int t, count=0;
    @(negedge clk) disable iff (!rstn)
    (my_seq, t = my_timing -1 ) |->  strong( // <--- the strong !!!!! 
          ##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t));
  endproperty

From my SVA Handbook
Guideline: Qualify as strong properties that are sequences and have range delays or consecutive repetition operators (e.g., [*, [->, [= ) and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation. Example:


ap_ab_recommend: assert property(@ (posedge clk) a |-> strong([1:$] b)); // 
ap_ab_weak: assert property(@ (posedge clk) a |-> ([1:$] b)); // 
ap_abc_recommend: assert property(@ (posedge clk) a |-> strong(b[*) ##1 c); // 
ap_abc_weak: assert property(@ (posedge clk) a |-> (b[*) ##1 c); // 

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