Practicality of state-machine verification of speed-independent circuits
Steven M. Nowick, David L. Dill · 2003
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.>