Assertion to check req holds until ack

I want to do assertion check to make sure req stays high until ack high as shown in the waveform below. I try to do it like this but the assertion fail even when the condition is met. Can someone please point out what’s wrong with my assertion code?


property rfsh_req_wait_for_ack_p;
@(posedge clk)
$rose (dcr_usr_rfsh_req) |-> (dcr_usr_rfsh_req throughout ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);

In reply to lisa.lalice:
Your assertion does not meet the waveform you display
(dcr_usr_rfsh_req throughout ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));

If you want anassertion to meet your waveform where dcr_usr_rfsh_req==0 when
$rose(dsr_usr_rfsh_ack)==1 then do the following:

$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

In reply to ben@SystemVerilog.us:

$rose(dsr_usr_rfsh_ack)[->1]

As there is a $rose, isn’t the above assertion successful only in the first clock when ack==1 ?

Should we change the above assertion to as follows:

$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  (dsr_usr_rfsh_ack[->1] ##0 $fell(dcr_usr_rfsh_req)));

In reply to yourcheers:

In reply to ben@SystemVerilog.us:

$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  (dsr_usr_rfsh_ack[->1] ##0 $fell(dcr_usr_rfsh_req))); // without the $rose
//vs 
$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req))); // with the $rose
// COMMENTS
a |-> b[->1] // If b==1 in cycle a==1 the property is true 
             // If b==0 in cycle a==1,  then b[->1] is equivalent to $rose(b)[->1]
             // because when b==1 you do get a $rose(b).
a |-> $rose(b)[->1] // If b==1 in cycle a==1, then you have to wait till 
             // b==0 and then rises back to b==1 
// Bottom line: Little difference if you know that b==0 when a==1 

Ben SystemVerilog.us

In reply to ben@SystemVerilog.us:

Thanks ben, I was mistaken with the waveform where ack is not a pulse.

In reply to ben@SystemVerilog.us:

If you want anassertion to meet your waveform where dcr_usr_rfsh_req==0 when
$rose(dsr_usr_rfsh_ack)==1 then do the following:

$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));

Hi Ben, I’ve tried the assertion code you’d suggested me above but my assertion still fail

In reply to lisa.lalice:
Works for me!

ap_reqack: assert property(@(posedge clk) 
          $rose (req) |-> 
               req[*1:$] ##1 !req  intersect
               $rose(ack)[->1] ##0 $fell(req));  


  module top; 
    timeunit 1ns/10ps;
    `include "uvm_macros.svh"
     import uvm_pkg::*;
     bit clk, req, ack;   
     initial forever #10 clk=!clk;  
     ap_reqack: assert property(@(posedge clk) 
          $rose (req) |-> 
               req[*1:$] ##1 !req  intersect
               $rose(ack)[->1] ##0 $fell(req));  
 
      
       initial begin 
         repeat(200) begin 
             @(posedge clk);   
             if (!randomize(req, ack)  with 
             { req dist {1'b1:=5, 1'b0:=1};
               ack dist {1'b1:=1, 1'b0:=5};  
         }) `uvm_error("MYERR", "This is a randomize error");
         end 
         $finish; 
        end  
 endmodule     
  

In reply to ben@SystemVerilog.us:

It seems like my assertion only works when I assert it straight away instead of using property/endproperty

This is what I did and it works

rfsh_req_holds_until_ack_a : assert property(@(posedge clk) 
$rose (dcr_usr_rfsh_req) |-> dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req intersect $rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req));

This, on the other hand, the code that I did previously and it fails. It’s actually the same code I’m not sure why it fails

property rfsh_req_wait_for_ack_p;
@(posedge clk)
$rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);

In reply to lisa.lalice:

You need either a default clocking or a @(posedge clk) in either the property or in the assertion.

 

property rfsh_req_wait_for_ack_p;
@(posedge clk $rose (dcr_usr_rfsh_req) |-> 
  (dcr_usr_rfsh_req[*1:$] ##1 !dcr_usr_rfsh_req  intersect
  ($rose(dsr_usr_rfsh_ack)[->1] ##0 $fell(dcr_usr_rfsh_req)));
endproperty
rfsh_req_wait_for_ack_a : assert property(rfsh_req_wait_for_ack_p);

Ben systemverilog.us

In reply to ben@SystemVerilog.us:

Sorry Ben, that is a typo. I did add a default clocking in my assertion code and it still fail.

In reply to lisa.lalice:

Is default clocking the same as @(posedge clk or a different clock.

In reply to ben@SystemVerilog.us:

I used the same clock

In reply to lisa.lalice:
Check your code. If still correct, check with your vendor. The test code below gave me identical results for the whole simulation period. You can try it in your environment.
Also at Edit code - EDA Playground


  module top; 
    timeunit 1ns/10ps;
    `include "uvm_macros.svh"
     import uvm_pkg::*;
     bit clk, req, ack;   
     initial forever #10 clk=!clk;  
     default clocking @(posedge clk); 
     endclocking
     ap_reqack_direct: assert property(@(posedge clk) 
          $rose (req) |-> 
               req[*1:$] ##1 !req  intersect
               $rose(ack)[->1] ##0 $fell(req));  

     property p_reqack_default_clk;
        $rose (req) |-> 
           req[*1:$] ##1 !req  intersect
           $rose(ack)[->1] ##0 $fell(req);  
     endproperty 
     ap_reqack_default_clk: assert property(p_reqack_default_clk);  

     property p_reqack_with_clk;
      @(posedge clk) $rose (req) |-> 
         req[*1:$] ##1 !req  intersect
         $rose(ack)[->1] ##0 $fell(req);  
   endproperty 
   ap_reqack_with_clk: assert property(p_reqack_with_clk); 

   property p_reqack_with_clk2;
    $rose (req) |-> 
       req[*1:$] ##1 !req  intersect
       $rose(ack)[->1] ##0 $fell(req);  
 endproperty 
 ap_reqack_with_clk2: assert property(@(posedge clk) p_reqack_with_clk2);  
 
      
       initial begin 
         repeat(200) begin 
             @(posedge clk);   
             if (!randomize(req, ack)  with 
             { req dist {1'b1:=5, 1'b0:=1};
               ack dist {1'b1:=1, 1'b0:=5};  
         }) `uvm_error("MYERR", "This is a randomize error");
         end 
         $finish; 
        end  
 endmodule    
 
// Reesults  
...
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_reqack_direct" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(20): Assertion "ap_reqack_default_clk" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(27): Assertion "ap_reqack_with_clk" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(34): Assertion "ap_reqack_with_clk2" FAILED at time: 2,110ns (106 clk), scope: top, start-time: 2,090ns (105 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_reqack_direct" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(20): Assertion "ap_reqack_default_clk" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(27): Assertion "ap_reqack_with_clk" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(34): Assertion "ap_reqack_with_clk2" FAILED at time: 2,150ns (108 clk), scope: top, start-time: 2,130ns (107 clk)