Next Cycle Implication operator does not work

Regarding of the next cycle implication operator, it defined as if expr1 is true then expr2 must be true at the next evaluation point.
expr1 |=> expr2;

I’m trying to use next cycle implication operator in my example assertion.

property ncio_p
@(posedge clk)
  ~a |=> a;
endproperty

check01 : assert property (ncio_p);


But I got the error

this is my testbench for test of assertion.


timescale 1ns/1ps
        
module ex3;
reg clk;
reg reset;
reg  a; 
reg  b;      
        
initial begin
reset = 1;   
        
#11;    
             
reset = 0;   
             
             
             
end          
             
             
      
initial begin                                                       
clk = 0;                                                            
a= 0;                                                               
         
#13 a = 0;                                                          
#0  a = 1;                                                          
#2  a = 0;                                                          
#2  a = 1;                                                          
#2  a = 0;                                                          
#2  a = 1;                                                          
#2  a = 0;                                                          
#2  a = 1;                                                          
#2  a = 0;                                                          
end          
             
initial begin
b = '0;      
#13 b = 0;   
#2  b = 0;   
#1  b =1;    
#3  b =1;    
#1  b =1;    
#1  b =1;    
#1  b =1;    
#1   b = 0;  
             
end

always #1 clk = ~clk;

property cycle_delay_repetition_range;
@(posedge clk) disable iff (reset)
  ~a |=> a;
endproperty

check08 : assert property (cycle_delay_repetition_range);


But I got assert fail. Could you let me know what am I supposed to do to resolve this fail?

In reply to UVM_LOVE:

#1 a = 0;
#1 a = 0;

you assert that every time a=0 it will be '1 in the next posedge, but you provide sequence that caused a to be '0 the next posedge.

BTW, do you have initial block for clk? does clk toggle at all?

best of luck

In reply to UVM_LOVE:
Your testbench approach needs strong reconsiderations.
I suggest that you read my reply to this question:
Got this question:
Q: I need your advice in getting started with verification with systemverilog. I 've built various projects using Verilog and they was FPGA and ASIC synthesizable. what I need now is a road map that get me started with verification for example SVA , UVM and SV testbenches

A: To better respond to this question I am attaching a file that addresses the build of a verification plan, quick-and dirty partition testing, a reference to my co-author Srinivasan Venkataramanan on UVM, SVA and learning SVA.
I welcome comments from this community.
FIle also at LinkedIn
That link is a pdf file.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to OE93:

thanks I update some test initial sequence about ‘a’.
as you see, ‘a’ has to change as ‘1’ after disable period.
then the assertion is working I though. but problem is that assertion check in disable period.
so the assertion fail has propagated to non disable period.

I though that SVA does not sample in the disable period. but I SVA sampled the signal even in the disable period.

would you please let me know more detail about why time 13NS assertion has failed?
What am I supposed to do?

In reply to ben@SystemVerilog.us:

Hi Ben,
Now I’m reading your attached documents, So I think your are trying to tell me about SVA testbench must be conducted on non-blocking domain. so my blocking test sequence in initial statement is wrong.

Please correct me if I wrong.

In reply to UVM_LOVE:
…"SVA testbench must be conducted on non-blocking domain. "
[Ben] Not quite. However, typically, signals are assigned nonblocking and occur in the NBA region. Doing a #10 a=1; with posedge(clk) changing at t is same time when “a” changes can be problematic. It is also not stylist, though it should work; this is because within a time step signals used in an assertin are sampled in the Preponed region with the value just before the time step. What would be better is to do something like
@(posedge clk) a=1; // or a <=1;
Assertion sample signals in the Preponed region
See my paper 3) Understanding Assertion Processing Within a Time Step (Horizons Feb 27, 2023 issue)

This paper goes into detail about how evaluation regions should be handled by a simulator as described in the SystemVerilog LRM; this should give you a better understanding of how assertions work.


// I do the following: 
initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    bit v_a, v_b, v_err;
    repeat (200) begin
      @(posedge clk);
      if (!randomize(v_a, v_b, v_err) with {
        a  dist {1'b1 := 1, 1'b0 := 1}; // *****CAN USE signal a 
        // a changes in the Active region ************ OK 
        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");
      
      if(v_err==0) b<=v_b; else b<=!v_b; 
       // b changes in the NBA region  ****************
    end
    $finish;
  end




In reply to UVM_LOVE:
Look, I’m not a SVA expert at all, and it’s so embarrassing to even open my mouth when Ben is also responding to you…
But in general I have two basic recommendations:

  1. Add prints that describe the situation when the assert fails:
    asset () else $error(“expect that a = … but a = %b, b = %b, time = %t”, a,b,$time);
  2. Write a property with arguments, and send arguments when you assert:
    property check(clk,a)

    endproperty

assert property (c,x) else $error(…);
here c = clk and x = a.

In reply to OE93:

In reply to UVM_LOVE:
Look, I’m not a SVA expert at all, and it’s so embarrassing to even open my mouth when Ben is also responding to you…
But in general I have two basic recommendations:

  1. Add prints that describe the situation when the assert fails:
    asset () else $error(“expect that a = … but a = %b, b = %b, time = %t”, a,b,$time);

[Ben] You need the $sampled

asset property () else 
$error("expect that a = ... but a = %b, b = %b, time = %t", 
         $sampled(a),$sampled(b),$realtime);
  1. Write a property with arguments, and send arguments when you assert:
    property check(clk,a)…endproperty
    assert property (c,x) else $error(…);
    here c = clk and x = a.

Unless you see the need for reuse, which is usually rare, I do not use arguments because they make the assertion hard to read. For me, I have to mentally convert the formal arguments to the actual arguments while I am composing or reading an assertion.
Sorry, it gives me mental “fatigue!”
:)
Ben

In reply to ben@SystemVerilog.us:

Hi ben,

I’m trying to understand the behavior of disable iff. so I make one another example.


`timescale 1 ns / 1 ns
                 
module MUX       
(                
  input wire       CLOCK  ,
  input wire [3:0] IP1    ,
  input wire [3:0] IP2    ,
  input wire [3:0] IP3    ,
  input wire       SEL1   ,
  input wire       SEL2   ,
  input wire       SEL3   ,
  output reg [3:0] MUX_OP  
) ;              
                 
always @(posedge CLOCK)
  if (SEL1 == 1) 
    MUX_OP <= IP1 ;   
  else if (SEL2 == 1) 
    MUX_OP <= IP2 ;   
  else if (SEL3 == 1) 
    MUX_OP <= IP3 ;   

property mux_p1;             
@(posedge CLOCK)             
  $rose(SEL1) |=> ( IP1==MUX_OP);
endproperty                  
                 
property mux_p2;             
@(posedge CLOCK)             
  if (!$isunknown(SEL1))
    $rose(SEL1) |-> (IP1== MUX_OP);
    
endproperty     

check00 : assert property (mux_p1);
check01 : assert property (mux_p2);
                 

endmodule

`timescale 1 ns / 1 ns                                                            
                                                                                  
module T_MUX ;                                                                    
                                                                                  
  parameter PERIOD = 10 ;                                                         
                                                                                  
  reg        CLOCK  ;                                                             
  reg [3:0]  IP1    ;                                                             
  reg [3:0]  IP2    ;                                                             
  reg [3:0]  IP3    ;                                                             
  reg [2:0]  SEL    ;                                                             
  wire [3:0] MUX_OP ;                                                             
                                                                                  
                                                                                  
  MUX MUX1                                                                        
  (                                                                               
    .CLOCK  ( CLOCK  ),                                                           
    .IP1    ( IP1    ),                                                           
    .IP2    ( IP2    ),                                                           
    .IP3    ( IP3    ),                                                           
    .SEL1   ( SEL[0] ),                                                           
    .SEL2   ( SEL[1] ),                                                           
    .SEL3   ( SEL[2] ),                                                           
    .MUX_OP ( MUX_OP )                                                            
  ) ;                                                                             
                                                                                  
  always                                                                          
    begin                                                                         
      CLOCK <= 0 ;                                                                
      #(PERIOD/2) ;                                                               
      CLOCK <= 1 ;                                                                
      #(PERIOD/2) ;                                                               
    end                                                                           
                                                                                  
  initial                                                                         
    begin : TEST                                                                  
      integer i ;                                                                 
      @(posedge CLOCK);                                                           
      #(PERIOD/4); // Keep changes away from clock edges                          
      IP1 <= 4'b0001 ;                                                            
      IP2 <= 4'b0010 ;                                                            
      IP3 <= 4'b0100 ;                                                            
                                                                                  
      $display ("Starting 1st set of test vectors.");                             
                                                                                  
      for (i=0; i<=2; i=i+1)                                                      
        begin                                                                     
          SEL <= 1<<i ;                                                           
          #(PERIOD) ;                                                             
        end                                                                       
                                       
      for (i=0; i<=7; i=i+1)           
        begin                          
          SEL <= i ;                   
          #(PERIOD) ;                  
        end                            
                                       
      $display ("Finished 2nd set of test vectors.");
                                       
      $finish ;                        
    end                                
                                       
endmodule

I want to check MUX_OP has the same value of IP1 after unknown period.
So I generate 2 property.

property mux_p1;             
@(posedge CLOCK)             
  $rose(SEL1) |=> ( IP1==MUX_OP);
endproperty

mux_p1 is pass but mux_p2 does not.

property mux_p2;             
@(posedge CLOCK)             
  if (!$isunknown(SEL1))
    $rose(SEL1) |-> (IP1== MUX_OP);
    
endproperty

this Assertion has failed at time 15NS, How do I approach “disable iff” correctly?