COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Verified AIG Algorithms in ACL2
Verified AIG Algorithms in ACL2Add to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact William Denman. And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG , and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG -based approaches. We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF , etc., and developed reasoning strategies for verifying these algorithms. Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance. This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsThe Eddington Lectures Disaster Resilient Supply Chain Operations (DROPS) Workshop Series Showing of the Film 'STAR MEN' The obesity epidemic: Discussing the global health crisis second Different Views: E&D Lunchtime SessionsOther talksMathematical applications of little string theory Oncological imaging: introduction and non-radionuclide techniques Frontiers in paediatric cancer research Sustainability 101: how to frame it, change it and steer it Interconversion of Light and Electricity in Molecular Semiconductors Real Time Tomography X-Ray Imaging System - Geometry Calibration by Optimisation An SU(3) variant of instanton homology for webs The Partition of India and Migration Active bacterial suspensions: from individual effort to team work The frequency of ‘America’ in America Vest up! Working with St John's Medical Response Team |