On the symbolic analysis of combinational loops in circuits and synchronous programs

Abstract:
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 fixpoint of some function. Such a loop can be accepted if a unique fixpoint 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 Bdd-based 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 finite state machines.

Reference:

   @INPROCEEDINGS{halbwachs95a,
      AUTHOR={N. Halbwachs and F. Maraninchi},
      TITLE={On the symbolic analysis of combinational loops
            in circuits and synchronous programs},
      BOOKTITLE={Euromicro'95},
      ADDRESS={Como (Italy)},
      MONTH={\september\ },
      YEAR= 1995
   }

Postscript file