How to detect glitch using assertions?

I’m trying to create an assertion that will constantly check for a glitch in a signal. The assertion will not fail if glitches happen inside a time duration of 3ns, but it will fail if the signal changes after this duration.

This is what I did but it exits the assertion as soon as the first glitch happen. This is wrong because glitches may happen multiple times, like how combinational settling of gates create glitches.


//================= Glitch Detection ====================
property glitch_detect;
  time first_change;
  time duration = 3;

  @(req)
    (!req, first_change = $time) |=> (($time-first_change) <= duration)[*1:$];
endproperty : glitch_detect

glitch_detect_assert : assert property(glitch_detect)
else begin
  $error("Glitch detected on req signal!");
end
//=============== End of Glitch Detection ===============

Do you have any good assertion code for the problem?
I’m not actually sure if concurrent assertions are useful on glitch detection, or maybe immediate assertions are more useful. Please advise.
Thank you.

Regards,
Reuben

In reply to Reuben:

Hi Reuben,
Can you please explain more about triggering event of property?
I mean are you looking for change in req or posedge of req as a clocking event?
If you are looking for change in req then your assertion will vacously shown as passed whwenever req changes from 0 to 1.

Let’s skip the usual discussion here (I’m sure there’s a very good reason why your guys aren’t doing synchronous design, why you need to check combinatorial outputs, bla bla bla).

You only say that a glitch is allowed in the first 3ns, but how do you decide when a glitch is allowed again? This is something you also need to model. You can’t use concurrent assertions like this (at least probably not without a lot of extra support code). There are probably other (static?) tools out there that can help you with this.

In reply to Tudor Timi:

Hi Tudor,

The assertion is checking the output of an 8-bit switch/mux. (I just put req but it is actually an 8-bit bus). This output will be fed to analog switch die. Therefore, glitch can’t happen on this output since a change on this value will change the selected signal of the analog die abrutply.

The reason why I decided to allow a glitch within the first 3ns is because of the inevitable wire delays that are present during gate level simulation. Then after this period, glitch should not happen because the selected signal of the analog die should not change abruptly. So my plan is after a posedge of clk, glitch can happen within 3ns, then after this period, glitch should not happen. The concurrent assertion will repeat for every posedge of clk.

About the “static” tools you mentioned, can you expound on this? I read something that formal verification tools can detect glitches, but I don’t understand how. I’m not that familiar in formal verification.

Thank you.

Regards,
Reuben

In reply to Reuben:

Hi Reuben,

Glitch can also be at positive value for req, in that case, you need to use something like this,

@(req)
  (1, first_change = $time) |=> (($time-first_change) <= duration)[*1:$];

I’ve tried with property as above, and it works for multiple glitch as well. If not same for you, can you provide a condition to experiment with?

Another way to detect negative glitch is,

property glitch_p;
  time t1;
  time t = 3;

  @(req)
    (!req, t1 = $time) |-> (req)[=1] ##0 (($time - t1) <= t);
endproperty

In reply to mayurkubavat:

Hi Mayur,

Yes, I think you are right. I should have used 1 instead of !req for the antecedent.
Anyway, what should I do to check if req is stable to a value of 1 after the 3ns period? My code above will only detect a single value transition then it exits the assertion check. I don’t know why it works for you. Take note that the 3ns is the period starting from the posedge of clk. In my code above, there is no clk so I think it’s totally wrong. If I put a clock, I don’t know how can I detect changes in req since the assertion will use the clock as a basis… Or maybe I can try using multiple clocks as basis. I’ll treat req as the other clock so that the assertion can detect changes from it.