Automatic verification of speed-independent circuits with Petri net specifications
David L. Dill, Steven M. Nowick, Robert F. Sproull · 2003
Asynchronous designs are of increasing interest because of the cost of broadcasting clocks over large areas of a chip. A tool for comparing implementations of speed-independent circuits with specifications is described. Petri nets are used throughout as a user-level description language. These are translated into trace structures, which can then be processed by an existing automatic verifier. This tool is applied to a nontrivial self-timed queue design.>