BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-89-387
       ENTRY:: November 08, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: SPECIFICATION AND AUTOMATIC VERIFICATION OF SELF-TIMED QUEUES
        TYPE:: Technical Report
      AUTHOR:: Dill, David L.
      AUTHOR:: Nowick, Steven M.
      AUTHOR:: Sproull, Robert F.
        DATE:: August 1989
       PAGES:: 25
    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.
       NOTES:: [Adminitrivia V1/Prg/19941108]
         END:: STAN//CSL-TR-89-387