An efficient verifier for finite state machines
- 1 March 1991
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 10 (3) , 326-334
- https://doi.org/10.1109/43.67786
Abstract
The correctness-checking problem of a finite-state machine is considered. The concept of machine cover is revived and used as the basis of the formulation of the verification problem of the design correctness of finite-state machines. The concept of machine cover enables the verifier to efficiently check the sufficiency. The verifier checks to see if the implementation is correct with respect to its specification, which is given as a form of finite-state machine. Since in general the state encoding information is not available for verification purposes, it is assumed that the encoding information is missing. An efficient algorithm for the verification problem is presented along with its implementation. Experimental results show that the approach is promising in terms of speedKeywords
This publication has 12 references indexed in Scilit:
- MUSTANG: state assignment of finite state machines targeting multilevel logic implementationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
- On the verification of sequential machines at differing levels of abstractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
- A new method for verifying sequential circuitsPublished by Association for Computing Machinery (ACM) ,1986
- Optimal State Assignment for Finite State MachinesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1985
- Hardware VerificationComputer, 1985
- A Temporal Logic for Multilevel Reasoning about HardwareComputer, 1985
- Verify: A program for proving correctness of digital hardware designsArtificial Intelligence, 1984
- Formal Design Verification of Digital SystemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1983
- A formal method for computer design verificationPublished by Association for Computing Machinery (ACM) ,1982
- An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic CircuitsIEEE Transactions on Computers, 1981