Variable ordering and selection for FSM traversal

The authors consider the problem of variable ordering in algorithms for verification of finite state machines (FSMs) for which the traversal is based on BDD (binary decision diagram) representation and image computation via implicit enumeration. They treat two separate BDD ordering problems: (1) min...

Full description

Saved in:
Bibliographic Details
Main Authors: Jeong, S-W, Plessier, B, Hachtel, G D, Somenzi, F
Format: Conference Proceeding
Language:English
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The authors consider the problem of variable ordering in algorithms for verification of finite state machines (FSMs) for which the traversal is based on BDD (binary decision diagram) representation and image computation via implicit enumeration. They treat two separate BDD ordering problems: (1) minimization of the representation of the next state function and the representation of the set of reachable states, and (2) a selection heuristic to reduce the complexity of the image computation problem by dynamic selection of the implicit enumeration splitting variables. In both problems they present theoretical results based on the algebraic structure of the next state functions, heuristic ordering methods, and favorable experimental results for problems with significant algebraic structure.