ABSTRACTS


The Constructive Semantics of Synchronous Circuits and Languages

G. Berry (Ecole des Mines) joint work with Tom Shiple (U.C. Berkeley)


A combinational circuit can be seen either as a system of boolean equations with input and output variables or as a graph of interconnected electrical gates with input and output wires. Usually, one requires combinational circuits to be acyclic. Acyclicity ensures existence and uniqueness of the boolean solution as well as electrical stabilization in bounded time, which is required in the synchronous circuit setting. However, acyclicity is too strong a condition for some practical applications. In particular, programs written in the imperative synchronous language Esterel are often compiled into cyclic but well-behaved circuits. We precisely define what it means to be well-behaved by showing the equivalence between three semantics for circuits: electrical stabilization in the inertial delay model, provability in a trivial constructive boolean logic, and definedness of a least fixpoint in Scott's three-valued boolean model. We present an efficient BDD-based algorithm to decide whether a circuit is consructive. Finally, we present the constructive semantics of Esterel and relate it to that of circuits.



1995 Asian Computing Science Conference, Thailand