SVA Question: How to check number of triggers within a period of time multiple times?

Hi,
I need help in developing a SVA checker that checks an interrupt being asserted accordingly.
Scenario: whenever singal “A” is triggered 5 times within 10ns, Interrupt “Q” will be asserted and cleared. This signal “A” may triggered multiple times throughout the simulation and all matched sequence must be checked.


property p1;
  ($rose(A))[->5] |-> Q[->1] ##[+] (!Q);
endproperty


property p2;
  time beg;
  (first_match($rose(A)),beg=$time) |-> Q[->1] ##0 (($time-beg)<=10);
endproperty

I’m stuck on how to combine these two checkers, can anyone help?

In reply to twhuang:
It’s OK not to combine them. In fact, multiple small assertions are better than big ones as they are easier to read, and debug.
On your (first_match($rose(A)),beg=$time) , why do you need the first_match()? you don’t.
If you really want to combine them, you can do the following:


property p1;
  realtime beg;
  ($rose(A),beg=$time) ##1 $rose(A)[->4] |-> // See comment 4 below, IMPORTANT!!!
     Q[->1]  ##0 ($realtime-beg)<=10 ##1 !Q[->1];  // !Q[->1] is same as ##[+] (!Q);
endproperty 

Some comments:

  1. Use realtime instead of time
  2. Don’t over abuse the use of parentheses. It makes your code very hard to read.
  3. Use small assertions.
  4. I see a potential issue with ($rose(A),beg=$time) ##1 $rose(A)[->4]
    That will work on the first rose(a), but every rose will start a new attempt (and assertion) I see potential failures. You need a differentiator that identifies the group of 5 rose(a). If your code does not have such a signal, you could create it.

bit go=1'b1;
function void set_go(bit x);
go = x;
endfunction
property p1;
realtime beg;
(go && $rose(A),beg=$time, set_go(0)) ##1 $rose(A)[->4] |->
Q[->1]  ##0 ($realtime-beg)<=10 ##1 !Q[->1];
endproperty
ap1: assert property(p1) set_go(1'b0); else set_go(1'b0);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • 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 0-9705394-2-8
  • 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

Hi Ben,

Thanks for your quick response & suggestions.
I’m aware of the issue that you mention in no.4, and now I learn a new way to control & write clever SVA checkers.
It works after fixing one typo in the last line that should reset go to 1’b1.

However, after I run more scenarios, I encounter more issues:
(1) When “A” is triggered more than 5 times, “Q” remains high until it’s cleared.
Let’s say “A” is triggered 8 times, the 3 extra triggers will be accumulated to next group of “A” and evaluated that timing range which exceed 10ns will cause checker to assert fail.
I can solve this by setting go to 1 whenever “Q” is cleared.


  (go && $rose(A),beg=$time, set_go(0)) ##1 $rose(A)[->4] |->   
     Q[->1]  ##0 ($realtime-beg)<=10 ##1 (!Q[->1],set_go(1))

(2) But then what if assert condition not meet (let’s say “A” only triggers 4 times), how do I add the condition to set go to 1 whenever 10ns passed since the last pulse without affecting the first condition (1)?

Thank you very much for your help and I hope this will help others too. :-)

In reply to twhuang:
For the (2) condition when “A” triggers <5 times:
I tried to toggle ‘go’ bit by adding an always block that waits idle time for >10ns and resets ‘go’ to 1, however, the evaluation of assertion already started and will affect the following group of “A”, resulting a checking fail even the 2nd group of "A"s meets the requirement. (o,O)?


int idle_cnt;
always @(posedge clk_1ns)
begin
  if(!go) begin
    if(A) idle_cnt = 0;
    else idle_cnt++;
    if(idle_cnt > 10) go = 1;
  end
  else idle_cnt = 0;
end

In reply to twhuang:
Use the action block


ap: assert property(  
(go && $rose(A),beg=$time, set_go(0)) ##1 $rose(A)[->4] |->   
     Q[->1]  ##0 ($realtime-beg)<=10 ##1 (!Q[->1],set_go(1)) else set_go(1);

In reply to ben@SystemVerilog.us:

Hi Ben,
With the action block “else set_go(1)” doesn’t quite get the checker behavior that I want,
since the assertion is already fired at first trigger of “A”, and if “A” only triggers <5 times over 10ns (which will not trigger “Q”), it will assert fail at the following group of x5 "A"s because the consequent condition (<=10ns) not met.
eg.
A,A,A,A,…10ns…,A,A,A,A,A,Q
start------------------------------->fail (over 10ns)

Thus, I add assertion controls into my always block to turn off the checker temporarily in this condition and finally get the checker to work:


int idle_cnt;
always @(posedge clk_1ns)
begin
  if(!go) begin
    if(A||Q) idle_cnt = 0;
    else idle_cnt++;
    if(idle_cnt > 10) begin
      go = 1;
      $assertkill(1,ap);
    end
  end
  else idle_cnt = 0;
  if(A) $asserton(1,ap);
end

Anything that I should note for using these assertion system tasks?

In reply to twhuang:

  1. What you are checking is a protocol that has a set of requirements. Typical protocols have a scheme to identify the start of a frame. It is really THAT start-of-frame that you need to use as enabler for your assertion.
  2. Since you understand the requirements, it is your task to figure out how to take advantage of the frame identification. My goal here is to just guide you in the right direction.
  3. Comments on your solution: just looking at it, it seems problematic.

int idle_cnt;
always @(posedge clk_1ns)
begin
if(!go) begin
if(A||Q) idle_cnt = 0;
else idle_cnt++; // YOU SHOULD USE NONBLOCKING ASSIGNMENTS
// idle_cnt <= idle_cnt + 1'b1;
if(idle_cnt > 10) begin
go = 1;  // YOU SHOULD USE NONBLOCKING ASSIGNMENTS
$assertkill(1,ap);
end
end
else idle_cnt = 0;
if(A) $asserton(1,ap); // Wouldn't you miss the 1st rose(A)?
//The asserton is after the Preponed region.
end

Your best solution is to use supporting logic as derived from the protocol to define the start of frame, and the frame itself.
You can also write additional assertions about the frame.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • 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 0-9705394-2-8
  • 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

In reply to ben@SystemVerilog.us:
Hi Ben,

Thanks for your correction.
What I’m implementing is just a checker that checks the interrupt behavior when a fault occurs at any time, there isn’t really a start of frame. I tried to generalize the scenario so the requirements may not be that clear.
Nevertheless, I appreciate your help to get me started in this checker implementation. I know this simple solution may seem to be problematic, and I believe there’ll be more elegant ways to implement such checker.
I’ll continue to look into it and improve it.

Thanks.