Various implementations of a method, system and computer program product receive a circuit model that can include an asynchronous crossing between a first set of one or more logic components in a first clock domain and a second set of one or more logic components in a second clock domain. A shadow network can be constructed that corresponds to the asynchronous crossing, where the shadow network includes at least one of an asynchronous transition detector, an asynchronous sample detector, and a metastability timer. The shadow network can include shadow network signals corresponding to signals of the asynchronous crossing.