Improving symbolic traversals by means of activity profiles

Symbolic techniques have undergone major improvements in the last few years. Nevertheless they are still limited by the size of the involved BDDs, and extending their applicability to larger and real circuits is a key issue. Within, this framework, we introduce “activity profiles” as a novel technique to characterize transition relations. In our methodology a learning phase is used to collect activity measures, related to time and space cost, for each BDD node of the transition relation. We use inexpensive reachability analysis as learning technique, and we operate within inner steps of image computations involving the transition relation and state sets. The above informations can be used for several purposes. In particular, we present an application of activity profiles in the field of reachability analysis itself. We propose transition relation subsetting and partial traversals of the state transition graph. We show that a sequence of partial traversals is able to complete a reachability analysis problem with smaller memory requirement and improved time performance