Unbounded Scalable Hardware Verification
Monday, May 02, 2016|
2:00pm - 4:00pm
3725 Beyster Bldg.
Add to Google Calendar
About the Event
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.
Sponsor(s): Professor Karem A. Sakallah
Open to: Public