The present invention is directed to methods for verifying adequate synchronization of signals that cross clock environments. According to one exemplary method, a circuit under design includes a plurality of functional elements and a plurality of clock environments, and has one or more signals passing from one clock environment to another therein. The method includes the steps of (i) modelling at least one of the functional elements to have an unknown state as an output for a predetermined time after a timing event of a clock signal, (ii) simulating the circuit, and (iii) determining which functional element is a synchronizer to thereby identify if there is a synchronization problem for a signal passing from one clock environment to another.