Techniques for Implicit State Enumeration of EFSMs

Autor:	Thomas R. Shiple, James H. Kukula, Adnan Aziz
Rok vydání:	1998
Předmět:	Finite-state machine Computer science Binary decision diagram Datapath Enumeration State (computer science) Algorithm Formal verification Presburger arithmetic Integer (computer science)
Zdroj:	Formal Methods in Computer-Aided Design ISBN: 9783540651918 FMCAD
DOI:	10.1007/3-540-49519-3_30
Popis:	BDD-based implicit state enumeration usually fails for systems with wide numeric datapaths. It may be possible to take advantage of higher level structure in designs to improve efficiency. By treating the integer variables as atomic types, rather than breaking them into individual bits, one can perform implicit state enumeration using Presburger arithmetic decision procedures; the complexity of this approach is independent of the width of the datapath. Since BDDs grow with the width of the datapath, we know that at some width BDDs will become less efficient than Presburger techniques. However, we establish that for widths of practical interest, the BDD approach is still more efficient.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::99f0aec156bdaf1ed6314bc26f2b2b8b https://doi.org/10.1007/3-540-49519-3_30 Zobrazit plný text záznamu