Assertion

I am confused between these 2 assertion

property p1
@(posedge clk) ~reg |-> ##3 ack;
endproperty

property p2
@(posedge clk) ~reg |=>##3 ack;
endproperty

In reply to fuwad khan:

The difference is one clock cycle.
“|->” is overlapping implication, which means the the matching endpoint point for the LHS sequence, the antecedent, is the same cycle to start the property on the RHS, the consequent.

“|=>” is non-overlapping implication, which means one cycle after the the matching endpoint point for the LHS sequence, the antecedent, will be the starting cycle for the property on the RHS, the consequent.

p2 is equivalent to

property p2;
@(posedge clk) ~req ##1 1'b1 |-> ##3 ack;
endproperty

I want to know that in p1 after evaluation of LHS then it will take ##2 or ##3 to evaluation RHS.
As in same cycle implication evaluation start at same cycle so what is the exact delay it will take.

In reply to fuwad khan:

In about the same amount of typing for your question, you could have tried a small example

module top;
   bit clk,req=1,ack;
   p1: assert property(@(posedge clk) !req|-> ##3 ack);
   p2: assert property(@(posedge clk) !req|=> ##3 ack);
   always #1 clk++;
   task stim(bit r,a);
      @(posedge clk) req <=r;ack=a;
   endtask 
   initial begin
      stim(0,0);
      stim(1,0);
      stim(1,0);
      stim(0,1);
      stim(1,0);
      stim(1,0);
      stim(1,0);
      stim(1,0);
      stim(1,1);
      $finish;
   end
endmodule : top

In reply to fuwad khan:
A few comments:

  1. For readability, use the unary logical negation operator (!) instead of the Bitwise unary negation (~). Thus, istead of ~req use !req.
  2. The ##n in SVA is equivalent to the following in a task:

repeat(n)  @(posedge clk);
// SVA requires the "n" to be a constant after elaboration.  The task does not.

See my paper at
https://verificationacademy.com/forums/systemverilog/paper-understanding-sva-engine-simple-alternate-solutions

Dave, In the generation stimulus vector, my preferred approach, even for simple examples, is to use constrained-random tests (I address the verification of assertions in my SVA book). Below is the template that I save in phase express auto text ( http://www.phraseexpress.com/ ), a great tool, BTW.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       if (!randomize(a, b)  with 
           { a dist {1'b1:=1, 1'b0:=3}; // Vary the distribution, as needed
             b dist {1'b1:=1, 1'b0:=2};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $stop; 
    end 
endmodule   

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


In reply to fuwad khan:

this is like

property p1
@(posedge clk) ~reg |-> ##3 ack; // this implies ~reg ##3 ack; whenever req is 0 then after 3 clock cycles ack must be 1
endproperty

property p2
@(posedge clk) ~reg |=>##3 ack; // this implies ~reg ##4 ack; whenever req is 0 then after 4 clock cycles ack must be 1
endproperty

you can use DAVE example , (added some dsiplay statement and made few changes) play using the stim(*) function with different value and you will get the concept

module top;
   bit clk =0,req=0,ack;
 
  p1: assert property(@(posedge clk) req|-> ##1 ack)
    $display("value of in P1 req %d and ack is %d" , req , ack , $time);;;
      else
        $display("ERROR:::value of in P1 req and ack is %d  %d and time is %t" , req , ack , $time);;;
    p2: assert property(@(posedge clk) req|=> ##1 ack)
    $display("value of in P2 req and ack is %d  %d " , req , ack);;;
      else
        $display("ERROR:::value of in P2 req and ack is %d  %d and time is %t" , req , ack , $time);;;
     
   always #1 clk++;
   task stim(bit r,a);
      @(posedge clk) 
     begin
       $display("inside function:: r %d a %d" ,r,a, $time);
       req =r;ack=a;
     end
   endtask 
   initial begin
     
     $display(" 0st", $time);
     stim(1,0);
     $display("crossed 0st", $time);
     #10
      $finish;
   end
endmodule : top
module asertion_eg;
  bit clk,a,b;
 
  always #5 clk = ~clk;
 
 
  initial begin
     a=1; b=1;
     a=0; b=0;
     a=1; b=0;
     a=0; b=0;
     a=1; b=1;
    #100;
    $finish;
  end
 
  property p;
    @(posedge clk) a |=> ##2 b;
  endproperty
 
 
  a_1: assert property(p);
   
 
  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
  end
endmodule

i tried this example with both same cycle implicatiojn(|->) and next cycle implication
(|=>) i am getting the same result where is the problem i am getting totally confused.

Your stimulus vectors have no clocks. You basically have one vector
a=1; b=1;
#100;
$finish;
end
Use the stimulus vectors that I have above with the randomize.
Ben systemverilog.us

yes i got what was the problem in my code thank you ben,dave.