System verilog assertion on asynchronous signal that kept calibrated

SystemVerilog
, ,
1

1347×272 8.1 KB

I’m writing assertion for source signal that is kept calibrated.
Source will eventually same edge with target.
The assertion will be:


module tb;
  property p1;
    int l_source;
    int l_target;
    realtime source_t;
    realtime target_t;
    @(posedge source) (1, source_t=$realtime, $display("**** Start **** \nsource_t=%0t",source_t)) |->
    @(posedge target) (1, target_t=$realtime, $display("target_t=%0t",target_t)) |->
    (1, l_source=int'(source_t)) |->
    (1, l_target=int'(target_t)) |->
    (l_source-l_target) == calibration_value;
  endproperty

  assert property (p1) $display("----- End -----"); else $display("----- End -----");
endmodule

Please ignore the assertion error for now, the issue is the middle assertion skip to the last one, since target is arriving first.

733×302 47.5 KB

Is there way to disable assertion when source > target? Or any idea to improve upon this?

2

In reply to warlocklw:
Try the accept_on

Note that this is the async accept_on that when true yields a vacuous result.
The action block resets the “cancel” bit to 0 on a pass or fail.
You don’t need the |-> or the l_source, l_target.
You may need the “timeunit 1ns; timeprecision 100ps;” // set values as needed
Your assertion checks that th 2 signals are in sync.


 module tb;
    bit source, target, cancel; 
    realtime calibration_value=0.1; 
    function void set_cancel(realtime src, trgt);
        if(src>trgt) cancel=1; 
        else cancel=0;       
    endfunction

    //disable assertion when source > target? 
    property p1;
      //int l_source;
      //int l_target;
      realtime source_t;
      realtime target_t;
      @(posedge source) accept_on(cancel) 
        (1, source_t=$realtime, $display("**** Start **** \nsource_t=%0t",source_t)) ##0
      @(posedge target) (1, target_t=$realtime, $display("target_t=%0t",target_t)) ##0 
        (1, set_cancel(source_t, target_t)) ##0
      //(1, l_source=int'(source_t)) |->
      // (1, l_target=int'(target_t)) |->
      (source_t -target_t) == calibration_value;
    endproperty
   
    assert property (p1) begin 
        set_cancel(1.0, 1.0); // reset cancel on pass
        $display("----- End -----"); 
      end 
      else 
      begin 
        set_cancel(1.0, 1.0);  // reset on fail
        $display("----- 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 - SystemVerilog - Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA - Part II
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
    SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
    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/
3

In reply to ben@SystemVerilog.us:
Another suggestion:


// Suppose that we create two properties. Also assume that the shift 
// between source and target is such that there is no all 0 gap, i.e., there is overlap.
  property p1;
      realtime source_t;
      realtime target_t;
      @(posedge source)  // source is first
        (!target, source_t=$realtime, $display("**** Start **** \nsource_t=%0t",source_t)) ##0
      @(posedge target) (1, target_t=$realtime, $display("target_t=%0t",target_t)) |->
      (target_t - source_t) <= calibration_value; //Should be a bound, not exct value
    endproperty

  property p2;
       realtime source_t;
      realtime target_t;
      @(posedge target) 
        (!source, target_t=$realtime, $display("**** Start **** \ntarget_t=%0t",target_t)) ##0
      @(posedge source_t) (1, source_t=$realtime, $display("source_t=%0t",source_t)) |->
      (source_t -target_t) <= calibration_value;
    endproperty

assert_property(p1 and p2) ; // or as two separate assertions.

// Would that work? If there is no overlap to start with, we could perhaps try something 
// with killing one property if the other one completes. not sure.
4

In reply to ben@SystemVerilog.us:

Thanks a lot Ben. This works for me.