Achieving Glitch-Free Clock Domain Crossing Signals Using Formal Verification, Static Timing Analysis, and Sequential Equivalence Checking.