Averroes: Scalable Formal Hardware Verification
He will describe the Averroes formal hardware verification system which exploits the power of two complementary approaches: counterexample-guided abstraction and refinement (CEGAR) of the design's datapath and the recently-introduced IC3 and PDR approximate reachability algorithms. Averroes is particularly suited to the class of hardware designs consisting of wide datapaths and complex control logic, a class that covers a wide spectrum of design styles that range from general-purpose microprocessors to special-purpose embedded controllers and accelerators. In most of these designs, the number of datapath state variables is orders of magnitude larger than the number of control state variables.
In the Media
Map apps may have changed our world, but they still haven’t mapped all of it yet. Specifically, mapping roads can be difficult and tedious: even after taking aerial images, companies still have to ...
Machine Learning and Data Analytics Symposium - MLDAS 2019 Building on the success of the three previous events , Boeing and QCRI will hold the fifth Machine Learning and Data Analytics Symposium (...
Visit by Antonio Torralba, who teaches machines to automate tasks that a human visual system can accomplish, is part of annual spring research update between QCRI and MIT-CSAIL.
Pact aims to apply data analysis and artificial intelligence techniques to solve humanitarian problems.
Well-known inventor of database recovery algorithms to deliver keynote at QCRI's first blockchain workshop.