Implicit state enumeration of finite state machines using BDD's
Top Cited Papers
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The authors propose a novel method based on transition relations that only requires the ability to compute the BDD (binary decision diagram) for f/sub i/ and outperforms O. Coudert's (1990) algorithm for most examples. The method offers a simple notational framework to express the basic operations used in BDD-based state enumeration algorithms in a unified way and a set of techniques that can speed up range computation dramatically, including a variable ordering heuristic and a method based on transition relations.<>Keywords
This publication has 5 references indexed in Scilit:
- Test generation for highly sequential circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- MIS: A Multiple-Level Logic Optimization SystemIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1987
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986