State Traversal guided by Hamming Distance Profiles.
Andreas Hett, Christoph Scholl, Bernd Becker · 2000
Abstract In the last years symbolic techniques have revolutionized reachability analysis. Handling large, industrial designs is a key issue, involving the need to focus on memory consumption for BDD representation as well as time consumption to perform symbolic traversals of finite state machines. In this paper we address the problem of reachability analysis for large finite state machines, introducing a novel technique that performs reachability analysis using a sequence of "Hamming Distance guided " partial traversals based on dynamically chosen prunings of the transition relation. The efficiency and stability of our approach is demonstrated by experimental results: We succeed in completing reachability problems with significantly improved time performance and smaller memory requirements. 1 Introduction One of the major problems in functional design verification is to decide whether a set of target states of a given Finite State Machine (FSM) can be reached from a set of initial states. Forward state space traversal techniques solve this problem by an iterative fixed point computation of all reachable states starting from the initial states. A significant number of techniques and refinements have been developed to make Reachability Analysis applicable for large designs. Especially symbolic techniques which avoid an explicit representation of the set of reachable states and of the FSM transition relation by using BDD representations increased the problem sizes which could be solved by FSM traversal [8, 11, 13, 3].