Embodiments of the present invention generate equations that model a synchronous circuit that contains sequential elements, which may include transparent elements, and a plurality of multiple-phase clocks. Phase-related information is assigned to nodes of the circuit. The phase-related information describes input and output characteristics at nodes of the circuit as the characteristics relate to clock phases. Equations are formed that model signals at the circuit nodes based on the phase-related information.