Assertion failed with delay operator

Trying to understand assertion with delay operator


module asertion_ex;
  bit clk,a,b;
  
  always #5 clk = ~clk; //clock generation
  
  //generating 'a'
  initial begin 
        a=1; b=1;
    #15 a=0; b=0;
    #10 a=1; b=0;
    #10 a=0; b=0;
    #10 a=1; b=1;
    #10;
    $finish;
  end
  
 a0:assert property  
    (@(posedge clk) a |-> ##1 !b ##1 b ##1 !b);
endmodule

Why does a0 assertion fail at 15ns and 35ns ?

a and b are ‘high’ at 5ns. and a and b are ‘low’ at 15ns.
‘|-> ##1’ is the same ‘|=>’ Right?

In reply to UVM_LOVE:
The application if your test vectors because you are very much dependent on the sequence in which the simulator processes the code. You have:


always #5 clk = ~clk; //clock generation
  //generating 'a'
  initial begin 
        a=1; b=1; 

If a=1 is processed by the simulator BEFORE the (@(posedge clk) a |-> …
the sampled value of “a” is 1. HOWEVER,
If a=1 is processed by the simulator AFTER the (@(posedge clk) a |-> …
the sampled value of “a” is 0, the defaulted value in the declaration.
SVG has explicit timing regions to prevent this issue. See my answer at
https://verificationacademy.com/forums/systemverilog/understanding-systemverilog-scheduling-better
The key here is that your test vectors should be applied with a nonblocking assignment (i.e., the <= ). This is the template I use to check assertions. I modify the variables and constraints as needed.


module top;
  timeunit 1ns; timeprecision 100ps;
  `include "uvm_macros.svh"
  import uvm_pkg::*;
  bit clk, a, b, reset_n;
  default clocking @(posedge clk); endclocking
  initial forever #10 clk = !clk;
  initial begin
    $timeformat(-9, 0, " ns", 10);
    $display("%t", $realtime);
  end
  always @(posedge clk) begin
  end

  property p;
    int v;
    @(posedge clk) disable iff (reset_n == 0) a |-> b;
  endproperty

  initial begin
    bit v_a, v_b, v_err;
    repeat (200) begin
      @(posedge clk);
      if (!randomize(
              v_a, v_b, v_err
          ) with {
            v_a dist {
              1'b1 := 1,
              1'b0 := 1
            };
            v_b dist {
              1'b1 := 1,
              1'b0 := 2
            };
            v_err dist {
              1'b1 := 1,
              1'b0 := 15
            };
          })
        `uvm_error("MYERR", "This is a randomize error");
      a <= v_a;
      if (v_err == 0) b <= v_b;
      else b <= !v_b;
    end
    $finish;
  end
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    Understanding and Using Immediate Assertions
    Understanding and Using Immediate Assertions | Verification Horizons - December 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Thank you Ben. (I’m new for SVA)
Actually I’m confused that assertion result will be depended by the EDA simulator and to prevent issue assertions Test vectors have to be used in Non-Blocking( =>).

I’m trying to execute some examples from https://verificationguide.com/systemverilog/systemverilog-assertions/
then this is not good example for me as your recommend.

Actually, I would like to make a test vector as the below


task test;
...
    @(negedge scl);  #(`WAIT) sda = 1;
    @(posedge scl);  #(`WAIT) sda = 0;
    #10;
    for(int i=0; i<4; i++)#(`WAIT) sda = 1;
...


In reply to UVM_LOVE:
The tools are OK. SV has specific zones when in a time step different types of activities are processed. This is needed because a simulator tool computes sequentially but must emulate concurrency. The style used in that link can lead to errors depending on how a tool handles the model, and this is not a violation of 1800. There is nothing in 1800 that specifies in which sequence the following code is handled:


iniital forever #10 a=!a; 
initial forever #10 b=!b;
iniital foever  #5 ck=!ck;

SVG 1800 has explicit timing regions to prevent this issue. See my answer at
https://verificationacademy.com/forums/systemverilog/understanding-systemverilog-scheduling-better

In reply to ben@SystemVerilog.us:

Through, Understanding and Using Immediate Assertions | Verification Horizons - December 2022 | Verification Academy.

I summarized that my issue.

Test vector can build-up in Blocking assignment. but assertion result depends on Tool
such as something Tool will work
If a=1 is processed by the simulator BEFORE the (@(posedge clk) a |-> …
the sampled value of “a” is 1. HOWEVER,
If a=1 is processed by the simulator AFTER the (@(posedge clk) a |-> …
the sampled value of “a” is 0, the defaulted value in the declaration.

To prevent assertion result issue depends on the Tool, you recommend that Non-Blocking assignment would use in Test vector.

Am I correctly understand your answer?

In reply to UVM_LOVE:

  • SVG requires proper coding style, regardless of the tools.
  • Bad coding style may yield unpredictable results depending upon how tools computes the model per 1800 rules; meaning GIGO. Bad style |-> unpredictable results
  • 1800 provided the right syntax and guidelines to emulate cncurrency.

Test vector can build-up in Blocking assignment.

NO. You need to use nonblocking assignment or clocking blocks (see 1800)

but assertion result depends on Tool such as something Tool will work

I didn’t say that. The scheduling of the model is well defined. My figure in that paper is a graphical view of what and where things are processed.

If a=1 is processed by the simulator BEFORE the (@(posedge clk) a |-> …
the sampled value of “a” is 1. HOWEVER,
If a=1 is processed by the simulator AFTER the (@(posedge clk) a |-> …
the sampled value of “a” is 0, the defaulted value in the declaration.

I was providing an example of the issue if coding styles are incorrectly used.

To prevent assertion result issue depends on the Tool, you recommend that Non-Blocking assignment would use in Test vector.

The commendation is a language recommendation, not a tool problem.
Example: You put your car in NEUTRAL gear, press the gas pedal, and then complain that the car is not moving forward. You wonder why, and then you blame the car.

SYstemVerilog is a nice flexible language, but if used incorrectly can yield unpredictable results. blocking assignments occur when they are seen, nonblocking assignement are queued and then processed in the nonbloking region.
Ben