Assertion signal high between two triggers

SystemVerilog
1

Hi all,

I’m wondering if it’s possibile to use SVA for this check:
vld must be high when sop is high, until eop is high (this assertion must be evaluated only when rdy is ‘1’).
But sop, eop can be ‘1’ in the same clock cycle (so vld is ‘1’ only for 1 clock cycle).

I tried with:

assert property (@(posedge clk) disable iff (!reset_n) (($rose(sop) && vld && rdy) |-> vld && rdy s_until ($rose(eop) && rdy)))

but it fails when rdy goes down or when sop and eop are in the same clock cycle.
Any suggestion?

2

In reply to alexkidd84:
You need the s_until_with.
You also said that vld must be high when sop is high, until eop is high (this assertion must be evaluated only when rdy is ‘1’). I understand that to mean the following:
(vld && rdy) || !rdy s_until_with eop.
As a matter of preference, I don’t like to use the until operator because it is subject to interpretation, meaning that (a until b) is translated into
property (a) is true at all cycles until property (b) is true.
See Assumption for req and ack and response interface | Verification Academy
I also afdrees those operators in my paper
Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy



module top;
  timeunit 1ns;  timeprecision 100ps;    
  `include "uvm_macros.svh"   import uvm_pkg::*;
  bit clk, reset_n=1, sop, vld, rdy, eop;
  initial forever #10 clk = !clk;
  // vld must be high when sop is high, until eop is high (this assertion must be evaluated only when rdy is '1').
  ap1: assert property (@(posedge clk) disable iff (!reset_n)
     $rose(sop) && vld && rdy |-> vld && rdy s_until ($rose(eop) && rdy));

  ap2: assert property (@(posedge clk) disable iff (!reset_n)
     $rose(sop) && vld && rdy |-> (vld && rdy) || !rdy s_until_with ($rose(eop) && rdy));

  ap3: assert property (@(posedge clk) disable iff (!reset_n)
     $rose(sop) && vld && rdy |->strong( ((vld && rdy) || !rdy)[*1:$] 
                                         intersect ($rose(eop) && rdy)[->1]));
    
  initial begin
    bit v1, v2, v3, v4; 
    $timeformat(-9, 0, " ns", 10);
    repeat (300) begin
      @(posedge clk);
        if (!randomize(v1, v2, v3, v4) with {
        v1  dist {1'b1 := 1, 1'b0 := 4};
        v2  dist {1'b1 := 4, 1'b0 := 1};
        v3  dist {1'b1 := 3, 1'b0 := 1};
        v4  dist {1'b1 := 1, 1'b0 := 3};
      }) `uvm_error("MYERR", "This is a randomize error");
      sop<=v1; vld<=v2; rdy<=v3; eop<=v4; 
    end
  end
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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 | Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/