1. A method for digital circuit design, comprising the steps of: providing a circuit design in the form of a hardware description language; performing a simulation of the circuit design by setting out, for multiple points of time during execution of the circuit design, a control state of the circuit design and a program state of the circuit design, wherein the control state includes program counters and pending variable updates, including: assigning a symbol to each signal of the circuit design; and executing a symbolic simulation of the circuit design including at least one non-unrollable loop; based on the simulation of the circuit design in the form of the hardware description language, identifying and capturing at synchronization points where contents of the control state are identical: a combinational logic expression of the simulation output; and next state functions of the simulation; and based on said identifying and capturing, generating a formal model of the circuit design, wherein the simulation of the circuit design identifies the synchronization points in time based on having identical contents of at least one variable of the control state.