Tutorial

Warren Hunt - Verification of the VIA (Centaur) Nano Microprocessor using the ACL2 Theorem-Proving System

We describe our use of the ACL2 theorem-proving system for formally verifying properties of the VIA Nano microprocessor. To validate Nano circuit models, we translate the Nano Verilog into in our formally defined HDL. We write specifications in the ACL2 logic, and mechanically verify HDL descriptions using a combination of automated and theorem-proving techniques. Using the ACL2 theorem prover, we orchestrate the use of BDDs, AIGs, SAT, and symbolic simulations techniques. Our system has been integrated into the Centaur design toolflow; this includes rapid and regular translation of the Nano design into our framework and daily regression runs.