UC Santa Barbara

This thesis addresses the problem of behavioural identification and timingverification for asynchronous, pulse-gate circuits. In particular, the design of very high performance logic and control functions such as time-to-digital, data-recovery, pipeline and FIFO control logic are targeted. The objective of this work is to produce models that are sufficiently general to include these hand designed circuits, amenable to automatic timing verification and, if possible, encompass known pragmatic techniques for asynchronous closure.

To achieve this timing verification a pair of timing models are proposed. The ``unit time'' model models the local behaviour of the circuit, and a ``phrase'' model models the communication between the unit timed regions. The phrase model also leads to a model for system level behaviour.

The ``unit time'' model allows the abstract system behaviour derived from symbolic simulation of the circuit as the specification. This step uses the special behaviour of pulse gates to create the symbolic abstraction, thus identifying possible nominal `states' of model predicted behaviour and through this agreed behavioural convention the behaviour predicted by the model should agree with designer intended behaviour.

Next ``phrases'' are introduced as a model for communication between coherent unit timed regions, while the whole ensemble system need not be coherent. The whole system can be examined at a global level by modelling the set of phrases potentially currently occurring and which phrases result from these. This describes a path towards system level verification to ensure that behavioural escape does not occur due to overlaps of predicted local behaviours.

A ‘coherence depth’ property is defined to determine that gates in the local region are sufficiently connected over all logic cases for this model to be self sufficient. A formal proof that this property plus a set of critical path inequalities are sufficient to verify the timing of the system.

A computer tool is presented to derive the necessary timing constraints. Results from this tool are presented both to show the scale of problems it can handle, and that its constraints are in good agreement with SPICE for small circuits.