Anna Slobodova
ACL2 Seminar, Sept. 22, 2011

In recent years, leading microprocessor companies have made huge
investments to improve the reliability of their products.  Besides
expanding their validation and CAD tools teams, they have incorporated
formal verification methods into their design flows.  Formal
verification engineers require extensive training, and FV tools from
CAD vendors are expensive.  At first glance, it may seem that FV teams
are not affordable by smaller companies.  We have not found this to be
true.  This talk describes the formal verification framework we have
built on top of ACL2. This framework gives us the flexibility to work
on myriad different problems that occur in microprocessor design.  The
talk is a revised version of the talk given at MEMOCODE 2011.