Interrupt pulse checking using SVA

Hi,

I want to verify using SVA in VC formal tool that my interrupt pulse occurs or not
But my interrupt pulse width is less than one clock cycle.
How can i write my assertions to prove this property.

Thanks,
Reshma

In reply to Resh@Shar:

Formal tools to not handle asynchronous timing. You may need to check with your tool vendor for strategies to handle this kind of check,