Click here for the answer.

Many designs require crossing registers from one clock domain to another. Making sure clock domain crossings work requires a special type of proof, one where at least two incoming clocks are assumed. Examples of these types of proofs include asynchronous resets, word synchronizers, slave SPI devices, clock switches and asynchronous FIFOs.

The logic above attempts to assume the presence of two nearly identical clocks. It’s not quite sufficient, however, and as written it may cause proofs with those two clocks to fail. Can you identify any of the missing assumptions?

Hint: think about what it would take to get an assertion with a $past(X) construct referencing one of these two clocks to pass.