Assertion to verify a glitch in a signal

Question

Lets say there is a signal a . When the signal goes high, it has to stay high at least for three positive clock edges.

We can write the property as

property p;
@(posedge clk) $rose(a) -> a[*3];
endproperty

The property fails for the case below.

clk _ _ _ | = = = | _ _ _ | = = = | _ _ _ | = = = | _ _ _ | = = = |

a _ _ | = = = | _ _ | = = = = = = = = = = = = = = = = = =

This is not in accordance with the specification where a is going low in the middle but will be pulled high by the next posedge and hence the above assertion wont catch this.

Can anyone tell if there is any way to write assertion to catch this bug?

Thank you

Answer 1

You're mixing up stuff here. By writing a clocked assertion on signal a you're verifying that it is a synchronous signal that has a specific behavior.

Synchronous signals can glitch all they want in between clock edges, because they never get sampled there. This is exactly the reason why we use synchronous signals nowadays, i.e. to let the signal have a chance to settle to its value before we sample it.

If your signal a isn't supposed to glitch for some reason (I'm not a designer so I don't know where this would be useful), as far as I know you'd find this out using some kind of linting tool (e.g. Spyglass) that does a structural analysis on the HDL code.