Combinational loops are very likely to appear in circuits compiled from high level languages, especially imperative synchronous languages like Esterel, Statecharts or Argos.

These loops result from the fact that, both in circuits and in synchronous languages, the response of the system to incoming events can be viewed as a xpoint of some function. Such a loop can be accepted if a unique xpoint exists in any state which is reachable from the initial state of the system. Moreover, some\care-set", which expresses an assumption about inputs, should be taken into account. In this paper, we propose a complete Bddbased procedure to check the consistency of combinational loops and, when possible, to remove these loops without changing the semantics of the circuit. The method is presented in the framework of Boolean-encoded nite state machines.