Two assertions launched at different events finishing at the same event, how to make sure that they finish at the pulse of individual signals?

[pranavtoor]

Hi,

I have below assertion:

//////////////////////////////////////////////////////////////////////////
// Assertion 3: There should be a pulse of match_dv for each sot
property MatchDvPulseAfterSot;
  @(posedge clock) disable iff(!reset || DisableMatchDvPulseAfterSot_Flag)
  // When we get a valid sot
  $rose(sot & valid & ready) |->
    // Within 1 to 100 cycles we should see match_dv pulse
    ##[1:100] ($rose(MatchDv) ##1 !MatchDv);
endproperty : MatchDvPulseAfterSot
assert property (MatchDvPulseAfterSot);
//////////////////////////////////////////////////////////////////////////

Problem I am facing is that the assertion launches on two separate sot posedges (a , b), but both finish at the same event (c) instead of older one finishing on the current event and the next one should finish at the next event, so at the end of test i have one less pulse and the assertion fails.

packet sizes can be low or high and the range has to be 1-100 and if there are two small packets back to back there is a chance that two dv come together. maybe i am going about this in a wrong direction, please help me fix this assertion.

the wave looks like this:

Thanks

[pranavtoor]

In reply to verif_newbie:

I could find this way to get past the issue, if there is some other smarter way to achieve the same, then please help.

  // Assertion 3: There should be a pulse of match_dv for each sot
  int req_num, gra_num;
  // Prep for assertion
  always @(posedge clock) begin
    if (!reset) begin
      req_num = 0;
      gra_num = 0;
    end else begin
      if (sot & valid & ready) begin
        req_num++;
      end
      if (MatchDv) begin
        gra_num++;
      end
    end
  end
  property MatchDvPulseAfterSot;
    int curr_num;
    @(posedge clock) disable iff(!reset || DisableMatchDvAfterSot_Flag)
      // When we get a valid sot
      ($rose(sot & valid & ready), curr_num = req_num) |->
        // Within 1 to 100 cycles we should see match_dv pulse
        ##[1:100] ($rose(MatchDv) && (gra_num == curr_num)) ##1 !MatchDv;
  endproperty : MatchDvPulseAfterSot

  assert property (MatchDvPulseAfterSot)

[ben2]

In reply to verif_newbie:

Similar concept at Need help to write an assertion | Verification Academy
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy