Ignore a signal for few cycles before evaluating a condition - System Verilog Assertions

SystemVerilog
,
1

Hi All,

I’m trying to write a SVA for the following scenario :

I want to ignore the value of a signal ‘a’ for the the first 36 cycles and after that if signal ‘a’ goes high, signal ‘b’ should go high in the same cycle.

The signal ‘a’ which could potentially glitch for about 36 clocks and hence want to ignore it.

I couldn’t construct a reliable assertion model but I attempted to do this in the following way :

    property p_glitch;
        disable iff (!rstb)
        @(posedge clk) 1 |-> ##36 1 |-> ##[0:$] a |-> b;
    endproperty : p_glitch
  
    a_glitch : assert property(p_glitch);

Immediately there were several problems with this.

  1. The signal ‘a’ could potentially never happen as per the design which is okay. I want to check signal ‘b’ going high only if ‘a’ goes high. In my above assertion, I expect my assertion to fail if ‘a’ never toggles.

  2. Even when the signal ‘a’ toggles, the assertion is always in active state (never finishes)

Can you please explain what is going on with the above assertion and how to effectively write this?

Thanks in advance.

2

In reply to szy0014:

property p_glitch;
    disable iff (!rstb)
    @(posedge clk) ##36 a == b;
endproperty : p_glitch
  
a_glitch : assert property(p_glitch);
3

In reply to warnerrs:

In reply to szy0014:

property p_glitch;
disable iff (!rstb)
@(posedge clk) ##36 a == b;
endproperty : p_glitch
a_glitch : assert property(p_glitch);

The above assertion works, but it fails to express the true intent. Assertions should be made more readable In the above case:

  1. After the 1st attempt, it requires that at the 37th cycle a==b
  2. After the 2nd attempt, it requires that at the 38th cycle a==b
  3. … and so on

But the requirements are that the value of a signal ‘a’ be ignored for the first 36 cycles (after init), and after that (and forever), if signal ‘a’ goes high, signal ‘b’ should go high in the same cycle.
One can express this using the initialand the always property_expr statements.


initial ap_ab36: assert property(@ (posedge clk) ##36 1'b1 |-> always(a == b); );
// the "alwways property_expr" evaluates to true (vacuous or nonvacuous true) if 
// property_expr holds at every current or future clock tick.
// In that case, there is only ONE attempt starting at the very first posedge.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. 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
4

Thanks warners and Ben.

I was able to fix my assertion with these insights.