Unbounded Scalable Hardware Verification

Model-checking is a formal verification method that has been successfully applied to real-world

hardware and software designs. Model-checking tools, however, encounter the so-called state-

explosion problem, since the size of the state spaces of such designs is exponential in the number

of their state elements. In this thesis, we address this problem by exploiting the power of two

complementary approaches: (a) counterexample-guided abstraction and refinement (CEGAR) of

the design's datapath; and (b) the recently-introduced IC3 and PDR approximate reachability

algorithms. These approaches are well-suited to verify control-centric properties in hardware

designs consisting of wide datapaths and complex control logic. They also handle most complex

design errors in typical hardware designs. Datapath abstraction prunes irrelevant bit-level details

of datapath elements, thus greatly reducing the size of the state space that must be analyzed and

allowing us to focus on the control logic, where most errors originate. The induction-based

approximate reachability algorithms offer the potential of significantly reducing the number of

iterations needed to prove/disprove given properties by avoiding the implicit or explicit

enumeration of reachable states. Our experimental results on a number of industrial benchmarks

show that our approach is scalable and significantly outperforms bit-level verification.