Technical Report No. CSL--TR--89--387, pages 1-22 pp.. Stanford University (USA), Computer Systems Laboratory, 1989.
Abstract: Speed-independent circuit design is of increasing interest because of global timing problems in VLSI. The authors 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.
Keywords: self-timed queue; circuit design; VLSI; RAm; trace structure; queue cell chain; parallel chain; circular buffer.