A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal

We present a new logic-simulation-based algorithm on verifying safety properties of large sequential hardware designs. This algorithm explores the search space defined by partitioned internal circuit nodes. Two powerful features are proposed to increase the effectiveness during search space exploration and counterexample generation for verifying safety properties. These include 1) new search space constituted by internal nodes instead of state variables and 2) static learning on multiple nodes to further enlarge the target. These two features are integrated with the following techniques during our simulation: incorporation of a BCP (Boolean constraint propagation) engine for multiple nodes implication and multiple-time-frame GA (genetic algorithm) search. Because only logic simulation is needed in our algorithm, the computational effort is low. Experimental results on large benchmark circuits have shown that this logic-simulation-based verifier achieves significantly better results compared with existing formal verification tools and simulation-based methods