Proving properties of digital systems with abstraction-guided simulation

Functional verification is an important element in the design of digital systems. Model checking is a formal method to verify that the system satisfies a user-defined specification. Compared to simulation, model checking is much more exhaustive but also restricted in capacity. On the other hand, simulation is weak in detecting bugs that require long and complex sequences of events to be exposed. This thesis combines the virtues of model checking and simulation in an abstraction-refinement paradigm to mitigate the problems of either. Abstraction refinement is an iterative process of constructing a simplified model to verify the original model. In abstraction refinement, concretization---a process of deriving an error trace in the original model from the abstract ones---is used to refute a property. In this thesis, I describe a concretization algorithm based on simulation and SAT that efficiently refutes properties with very long error traces.;First, a simple algorithm is presented where the common concretization approaches are modified such that each transition of an abstract error trace is allowed to map to a sequence of transitions of the concrete error trace. To build a concrete error trace, the concrete model is simulated with fixed number of pseudo-random vectors. The subsequent optimization to the algorithm simulates the concrete model with flexible number of vectors that account for progress of the concrete trace towards the target.;The initial version of the algorithm is hindered by limited visibility, which often results in excessive backtracking or refinements of the abstract model. Two complementary enhancements to the algorithm address the issue. One, identifies invisible state variables whose addition to the abstract traces increases their predictive power; and two, combines SAT checks with pseudo-random simulation to construct the concrete trace.;Constraints on input vectors that are pseudo-randomly generated are often essential for the success of the concretization procedure. These constraints have to do with both, the primary inputs as well as invisible state variables. The final enhancement to the algorithm addresses both types of constraints.;Experimental studies demonstrate that the concretization algorithm presented in this thesis is key to refuting properties whose only counterexamples are very long traces.