UC Santa Barbara

In this paper, we address the problem of verification of pulsegate circuits. These circuits enable the design of very high performance logic functions such as data-recovery, pipeline and FIFO control logic. We adopt an approach of using an abstraction of the structure of the circuit as the specification. From this we can first obtain the nominal case behaviour of the circuit using conventional NFA exploration techniques adapted to distributed activity systems. Following the identification of possible nominal states, we identify the critical path inequalities that must be maintained to ensure this behaviour in implementation. This strategy mimics the abstract designer behavioral view of pulse gate activity and leads to a practical set of timing constraints for composite self-resetting and astable asynchronous logic circuits.