Sciweavers

DAC
1994
ACM

BDD Variable Ordering for Interacting Finite State Machines

14 years 4 months ago
BDD Variable Ordering for Interacting Finite State Machines
We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting finite state machines (FSMs). Orderings are derived from the communication structure of the system. Communication complexity arguments are used to prove upper bounds on the size of the BDD for the transition relation of the product machine in terms of the communication graph, and optimal orderings are exhibited for a variety of regular systems. Based on the bounds we formulate algorithms for variable ordering. We perform reached state analysis on a number of standard verification benchmarks to test the effectiveness of our ordering strategy; experimental results demonstrate the efficacy of our approach. The algorithms described in this paper have been implemented in HSIS, a hierarchical synthesis and verification tool currently under development at Berkeley.
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where DAC
Authors Adnan Aziz, Serdar Tasiran, Robert K. Brayton
Comments (0)