Assertion Question

SystemVerilog
, ,
1 
module assertion_example;
  bit clk =0 ;
logic a,b,c;
 
  always #10 clk = ~clk;
  property prop;
    @(posedge clk)
    $rose(a) |-> (b && !$isunknown(b)) until c;
  endproperty
 
  time_a: assert property(prop) $display("PASS");
    else
      $error("FAIL");
   
  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
    a=0;
    b=0;
    c=0;
   
    #10 a=1;
   
    b=1;
   
    # 5 b=1'bx;
   
    #50 c=1;
   
   #50 c=0;
 
    b=0;
    a=0;
    #100; $finish;
  end
endmodule

In above assertion code the assertion should failed at 10ns then why it is passing the assertion and failed at 30ns?

2

I think assertion variables are evaluated in the Observed region, by then b would have got the value of 1 (active region). Hence, assertion passes at the first posedge but fails at the next.

3

Yes this thing is happening like in first posedge it pass and in second posedge it fails but why it is again passing in third posedge and continue passing till the end of simulation?

4

I think is because of the “rose” nature. ‘a’ been rise only one, so the property been evaluated only one time.

1 Like