next up previous contents
Next: First Annual Meeting Up: Meeting at Madrid Previous: A Hoare-Logic for

Towards an Assumption-Commitment Calculus for Circuits

by Carlos Delgado Kloos, Universidad Politécnica de Madrid

Circuits usually perform the desired function only if some conditions are satisfied for the inputs. For instance, a flip-flop acts as a memory, provided that the transition from (1,1) to (0,0) never occurs. In the talk, we presented some half-baked ideas on how to define a calculus in which these conditions can be computed backwards from outputs to inputs for a stream-based language with combinators for serial, parallel and feedback composition.

As an example, the simple RS flip-flop is taken. A model is presented based on a three-valued logic (the boolean values 0 and 1 and a third ? for modeling the uncertainty of the exact value) and transport delay. Unwanted effects at the output (such as oscillation), imply conditions on the inputs, which imply conditions on other components on the environment. These conditions can be expressed in general as regular expressions of unwanted sequences.


Bernhard Moeller
Fri May 12 14:21:20 MET DST 1995