In: Digest of Technical Papers ot the IEEE International Conference on Computer-Aided Design, 1989, Santa Clara, CA, USA, pages 266-269. Piscataway, NJ, USA: IEEE Service Center, 1989.
Abstract: A state-machine verifier is described for speed-independent control circuits, using as an example an arbiter with reject. User-level behavioral descriptions are given as Petri nets, which are translated into trace structures, which are then automatically compared. The example verifies in two ways: first, the entire implementation is compared with a specification; second, the circuit is verified hierarchically according to the structure of the design. Performance figures are given.
Keywords: state-machine verification (of) speed-independent control circuit; arbiter (with) reject; trace structure; hierarchical verification; performance figures.