Checking a value in the consequent of an assertion

[cool_toad]

So I am trying to add a couple of assertions to my interface.

1. In the first one, I am checking for a value in the consequent of the assertion.

always @(posedge clk, negedge rst) begin
  if(~rst || ~signal_a) count <= 0;
  else if(signal_a) <= count = count + 1;
end 

property Check_Count;
  @(posedge clk)
    signal_a |-> ##[1:$] ~signal_a ##0 (count == 5);
endproperty

2. In the second one, I am using a local variable to perform the check,

property Check_Count;
  time t1, t2;
  @(posed clk)
    (signal_a, t1=$time) |-> ##[1:$] (~signal_a, t2=$time-t1) ##0 (t2 > 6us);
endproperty

Now both the assertions are triggered but the consequent never completes.

Can someone help figure out the problem here?

[ben2]

In reply to cool_toad:
With **signal_a |-> ##[1:] ~signal_a ##0 (count == 5);** If @count==3 signal_a==0, then that tread will fail, but there are other threads to test as a result of the ##[1:].
However, from your always block, the count gets reset.
What you are trying to specify is most likely the following:
in the consequent, whenever signal_a==0 then in the same cycle count==5 to do that you would need a first_match()
You could also use the goto

property Check_Count;
  @(posedge clk)
    signal_a |-> first_match(##[1:$] ~signal_a) ##0 (count == 5);
    // signal_a |-> ~signal_a[->1] ##0 (count == 5);
endproperty

property Check_Count;
  realtime t1, t2; // Use realtime instead of time 
  @(posed clk)
    (signal_a, t1=$realtime) |-> 
       first_match(##[1:$] (~signal_a, t2=$realtime-t1)) ##0 (t2 > 6us);
       // ~signal_a[->1] ##0 (1, t2=$realtime-t1) ##0 (t2 > 6us);
endproperty
 

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

[cool_toad]

That worked! Thanks for your help