Title :
Practicality of state-machine verification of speed-independent circuits
Author :
Nowick, S.M. ; Dill, D.L.
Author_Institution :
Comput. Syst. Lab., Stanford Univ., CA, USA
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 :
circuit CAD; circuit analysis computing; Petri nets; arbiter; behavioral descriptions; performance figures; specification; speed-independent circuits; state-machine verification; trace structures; Automatic control; Circuits; Computational modeling; Concurrent computing; Control systems; Design automation; Hardware; Humans; Laboratories; Wires;
Conference_Titel :
Computer-Aided Design, 1989. ICCAD-89. Digest of Technical Papers., 1989 IEEE International Conference on
Conference_Location :
Santa Clara, CA, USA
Print_ISBN :
0-8186-1986-4
DOI :
10.1109/ICCAD.1989.76950
