Algorithms for efficient state space search
Malay Ganai, Adnan Aziz · 2001
State space exploration has many applications including verifying safety properties, analysis of third-party RTL code to understand its behavior, generating tests to satisfy missing coverage, and justifying the reachability of a given state for a combinational equivalence checker. Unfortunately, state explosion is a common problem when exploring large designs. In practice, complete state space exploration, which would otherwise give a guarantee of correctness, is nearly impossible even for designs with a few hundred state elements. We focus on three strategies that address the problem of efficiently searching the state space of synchronous digital hardware designs starting from a designated initial state. Binary Decision Diagrams (BDDs) have been widely used in symbolic search strategies. Though BDDs are canonical, their size is critically dependent on variable ordering and the type of the functions they represent. We propose the use of a multi-level functional hashing scheme to a noncanonical two-input AND/INVERTER graph representation. Using this scheme, we could identify and eliminate on-the-fly a significant amount of functional redundancy in the graph; thereby allowing an efficient representation of circuits and Boolean expressions. Moreover, such representation is significantly less sensitive to the order in which it is built. We show that such representation outperforms previous noncanonical representation in combinational verification and increases the efficiency for Boolean reasoning. A simulation-based search strategy is simple and scales well but suffers from low design space coverage. Symbolic simulation, on the other hand, simulates a design over the complete input space. Previous approaches based on BDDs suffer from space-outs; while SAT-based approaches have been found fairly robust. We propose a SAT-based symbolic simulation algorithm using the AND/INVERTER graph representation. Experimental results on large examples show the effectiveness of the proposed technique over previous approaches. Using our approach we found real bugs in industrial designs which were previously undetected. Partial state exploration using guided techniques has become a subject of wide research. Guided state space search can use “state score-boarding” to guide the search towards the target states. We propose a rarity-based metric and several techniques based on that for state prioritization. We also propose techniques—target prioritization and on-the-fly lighthouse selection—based on “latch inertia” that lead to increased search efficiency. Coverage results on the large industrial designs show the effectiveness of these approaches. We integrated the proposed approaches in a framework SIVA that provides a robust and scalable alternative to complete verification of synchronous hardware designs. It enhances simulation-based search with symbolic algorithms for coverage-directed state space exploration. It provides a platform for future research.