Next Cycle Implication operator does not work

Question

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?

Answer 1

Solution

OE93

Full Access

10 posts

June 09, 2023 at 6:59 am

In reply to UVM_LOVE:

Quote:

#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

Answer 2

ben@SystemVerilog.us

Full Access

2880 posts

June 09, 2023 at 10:41 am

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 https://lnkd.in/gUVNrWa6
That link is a pdf file.

Ben Cohen

Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or https://rb.gy/ibks5p

Getting started with verification with SystemVerilog
https://rb.gy/f3zhh

Answer 3

UVM_LOVE

Full Access

292 posts

June 09, 2023 at 4:16 pm

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?

Answer 4

UVM_LOVE

Full Access

292 posts

June 09, 2023 at 6:17 pm

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.

Answer 5

ben@SystemVerilog.us

Full Access

2880 posts

June 09, 2023 at 8:04 pm

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)
https://systemverilog.us/vf/Understanding_assertion_processing.pdf
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

Answer 6

OE93

Full Access

10 posts

June 10, 2023 at 3:45 pm

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.

Answer 7

ben@SystemVerilog.us

Full Access

2880 posts

June 10, 2023 at 4:06 pm

In reply to OE93:

Quote:

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);

Quote:

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.

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

Answer 8

UVM_LOVE

Full Access

292 posts

June 11, 2023 at 12:26 am

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?

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Specification Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Solution

Portfolio

Explore

Siemens

Contact