Asynchronous behavior of a circuit is modeled by modifying latches in a netlist to add an extra port to the latches, e.g., a single-port latch is transformed into a dual-port latch. Each input port has an enable line and a data input. The data input in the added port is a feedback line from the latch output, and the enable line in the added port is the logical NOR of all of the original enable lines. By adding this extra latch port in the higher-level model, it becomes possible to introduce assertion logic to ensure that one and only one latch port for a given latch is ever active during the same simulation cycle. The model can then be tested earlier in the design methodology prior to the availability of the post-synthesis netlist. The model can also be used in both simulation and formal or semi-formal verification.