Reachability Analysis Using Partitioned-ROBDDs

Abstract

In this paper we address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned-ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques.

In our technique, the reachable state set is represented as a partitioned-ROBDD~\cite{narayan96b}. Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time.

We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned-ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned-ROBDDs as well as monolithic-ROBDDs cannot complete traversal, partitioned-ROBDDs can reach a significantly larger set of states.

For comments contact anarayan@ic.eecs.berkeley.edu