BDD Variable Ordering for Interacting Finite State Machines

A. Aziz, S. Tasiran and Robert K. Brayton

EECS Department
University of California, Berkeley
Technical Report No. UCB/ERL M93/71
October 1993

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/ERL-93-71.pdf

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 thee 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 preform 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.

BibTeX citation:

@techreport{Aziz:M93/71,
    Author = {Aziz, A. and Tasiran, S. and Brayton, Robert K.},
    Title = {BDD Variable Ordering for Interacting Finite State Machines},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1993},
    Month = {Oct},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/2431.html},
    Number = {UCB/ERL M93/71},
    Abstract = {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 thee 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 preform 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.}
}

EndNote citation:

%0 Report
%A Aziz, A.
%A Tasiran, S.
%A Brayton, Robert K.
%T BDD Variable Ordering for Interacting Finite State Machines
%I EECS Department, University of California, Berkeley
%D 1993
%@ UCB/ERL M93/71
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1993/2431.html
%F Aziz:M93/71