Glitch
Asynchronous glitches can be introduced during logic synthesis optimization of circuits that were safely implemented in RTL. Although rare, such issues can wreak havoc with the operation of the circuit in silicon, since at random times spurious transitions will occur in the circuit, most likely leading to functional failure. Glitches cannot be detected in RTL, and only very rarely can they be detected in gatelevel simulation - since the presence of the glitch is very tightly coupled to a very small asynchronous sampling window that many not be sensitized in GLS.
 
Detection and screening of glitches in Timevision breaks down into three parts
Detection of logic gates where a single asynchronous signal reconverges with itself
Detection of logic gates where two asynchronous signals converge, and
Detection of registers which have an asynchronous driver used to drive both the clock and data
 
Using the structure of the circuit (including synchronous registers inferred from the SDC) and user-directives, Timevision then formally proves whether an asynchronous glitch may occur in the circuit as a result of these conditions, and generates a counterexample of the glitch, as well as a search of which side inputs may be set to "non-switching" that would allow the glitch to pass formal verification.
 
A circuit exhibiting single-mode asynchronous glitch looks like this :
 
 
In this case, unless the register at the "top" of the circuit is synchronous or declared non-switching, a non-unate glitch can propagate from the asynchronous input on the left to the capturing regsiter on the right. Using formal verification, it's possible to prove that glitches can propagate or not propagate without needing to use simulation or painstaking manual methods.
 
Value Proposition
Asynchronous glitches can be chip killers – hard to find silicon bugs that are ghostly and impossible to find in functional simulation. Finding them before tapeout can save months of time-to-market and lost engineering time in the lab.