Exploiting functional dependencies in finite state machine verification
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper proposes a novel verification method for finite state machines (FSMs), which automatically exploits the relation between the state encodings of the FSMs under consideration. It is based on the detection and utilization of functionally dependent state variables. This significantly extends the ability of the verification method to handle FSMs with similar state encodings. The effectiveness of the proposed method is illustrated by experimental results on well-known benchmarks.Keywords
This publication has 8 references indexed in Scilit:
- Dynamic variable ordering for ordered binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Implicit state enumeration of finite state machines using BDD'sPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Heuristic minimization of BDDs using don't caresPublished by Association for Computing Machinery (ACM) ,1994
- Reducing BDD size by exploiting functional dependenciesPublished by Association for Computing Machinery (ACM) ,1993
- A new model for improving symbolic product machine traversalPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1992
- Verification of synchronous sequential machines based on symbolic executionPublished by Springer Nature ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986