Report Number: CSL-TR-89-387
Institution: Stanford University, Computer Systems Laboratory
Title: Specification and automatic verification of self-timed queues
Author: Dill, David L.
Author: Nowick, Steven M.
Author: Sproull, Robert F.
Date: August 1989
Abstract: Speed-independent circuit design is of increasing interest
because of global timing problems in VLSI. Unfortunately,
speed-independent design is very subtle. We propose the use
of state-machine verification tools to ameliorate this
problem. This paper illustrates issues in the modelling,
specification, and verification of speed-independent circuits
through consideration of self-timed queues. User-level
specifications are given as Petri nets, which are translated
into trace structures for automatic processing. Three
different implementations of queues are considered: a chain
of queue cells, two parallel chains, and "circular buffer"
example using a separate RAM.