Improving symbolic reachability analysis by means of activity profiles

Symbolic techniques have undergone major improvements in the last few years . Nevertheless, applications are still limited by memory size and time cons traints. As a consequence, extending their applicability to larger and real circuits is still a key issue. Within this framework, we introduce "activity profiles" as a novel techniqu e to characterize finite state machines described by their transition relat ion, In our methodology, a "learning phase" is used to collect activity mea sures. They are gathered, in an inexpensive way, for each binary decision d iagram node of the transition relation. They indicate the activity the node has been involved in, as an estimate of its correlation with space and/or time costs. The above information can be used for several purposes, In particular, we p resent an application of activity profiles in the field of reachability ana lysis, to enhance memory and time performance of traversals. More specifica lly, we use transition relation subsetting in order to traverse the state t ransition graph in a nonpurely breadth-first, guided and multistep fashion. Comparisons with other state-of-the-art approaches show that our sequence of partial traversals produces "best ever" results for all the large benchm arks analyzed.