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.
http://i.stanford.edu/pub/cstr/reports/csl/tr/89/387/CSL-TR-89-387.pdf