An edge clock model is used to capture states from a logic-level simulation of a circuit description. The states are captured at clock edges, or transitions, according to an edge clock model based on a clock specification for the circuit description. The captured states and associated attributes are used in formal verification of the circuit description. This approach helps to reduce or eliminate inaccuracies and other issues with other clock models such as a phase clock model. In one embodiment, a phase clock model can be used in addition to the edge clock model. In another embodiment, the edge clock states can be used to generate states according to different clock models, such as the phase clock model.