For the most recent entries see the Petri Nets Newsletter.

Specification and Automatic Verification of Self-Timed Queues.

Dill, D.L.; Nowick, S.M.; Sproull, R.F.

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.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography