Dec 3 (Fri) @ 4:00pm: "Automated Behavioral Identification and Timing Verification of Pulse Gate Systems," David Mc Carthy, ECE PhD Defense

https://ucsb.zoom.us/j/85803637927?pwd=ZUsvS3ltQjBBRVErMXUzOE5iN3ZCUT09

Abstract

This thesis addresses the problem of behavioural identification and timing verification 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. Conventional asynchronous logic often adopts local construction rules aimed at maintaining system coherence independent of circuit implementation. While simplifying the analysis, these conventions inherently limit the performance while often adding to the power overhead. In contrast, the proposed design style is aimed at high system performance where more general local timing verification closes the behaviour.

In this work, I propose a "unit time" model of 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.

A ‘coherence depth’ property is created to determine that gates in the local region are sufficiently connected over all logic cases for this model to be self sufficient. Following this, critical path inequalities are derived as constraints to ensure the abstract behaviour is followed in implementation. This strategy mimics the abstract designer behavioural view of pulse gate activity and leads to a practical set of timing constraints for composite self-resetting logic circuits.

This is achieved both by a formal proof showing that the coherence properties limit what kinds of timing constraints need to be explicitly considered, and implementation of a computer tool which measures circuit coherence depths and searches for timing paths that need to be covered.

Next I develop strategies for dealing with circuits larger than can be described as `coherent' by the above definition. The circuit is broken up into regions each of which does have this coherent property The boundary conditions of the coherent regions are described in terms of 'phrases' of coherent pulses. Firstly this extends the behavioural identification described above to ensure that the behaviours of the circuits on both side of the interface are compatible. It then allows timing verification between adjacent regions of local behaviour.

Lastly, I discuss how the whole system can be examined at a global level, 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 do not occur due to overlaps of predicted local behaviours.

Bio

David Mc Carthy is a PhD candidate in Electrical and Computer Engineering at the University of California at Santa Barbara. His research is on electronic design automation for asynchronous circuits. Before that he received his B.E and M.Eng.Sc from University College Cork in Ireland in 2013 and 2014 respectively.

Hosted by: Professor Forrest Brewer

Submitted by: David Mc Carthy <davidmc@ece.ucsb.edu>