BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified AIG Algorithms in ACL2 - Jared Davis - Centaur Technologi
 es and UT Austin
DTSTART:20130402T120000Z
DTEND:20130402T130000Z
UID:TALK44219@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:And-Inverter Graphs (AIGs) are a popular way to represent Bool
 ean\nfunctions (like circuits). AIG simplification algorithms can\ndramati
 cally reduce an AIG\, and play an important role in modern\nhardware verif
 ication tools like equivalence checkers. In\npractice\, these tricky algor
 ithms are implemented with optimized\nC or C++ routines with no guarantee 
 of correctness. Meanwhile\,\nmany interactive theorem provers can now empl
 oy SAT or SMT\nsolvers to automatically solve finite goals\, but no theore
 m\nprover makes use of these advanced\, AIG-based approaches.\n\nWe have d
 eveloped two ways to represent AIGs within the ACL2\ntheorem prover. One r
 epresentation\, Hons-AIGs\, is especially\nconvenient to use and reason ab
 out. The other\, Aignet\, is the\nopposite\; it is styled after modern AIG
  packages and allows for\nefficient algorithms. We have implemented functi
 ons for\nconverting between these representations\, random vector\nsimulat
 ion\, conversion to CNF\, etc.\, and developed reasoning\nstrategies for v
 erifying these algorithms.\n\nAside from these contributions towards verif
 ying AIG algorithms\,\nthis work has an immediate\, practical benefit for 
 ACL2 users who\nare using GL to bit-blast finite ACL2 theorems: they can n
 ow\noptionally trust an off-the-shelf SAT solver to carry out the\nproof\,
  instead of using the built-in BDD package. Looking to the\nfuture\, it is
  a first step toward implementing verified AIG\nsimplification algorithms 
 that might further improve GL\nperformance.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR