Title :
Verifying VIA Nano microprocessor components
Author :
Hunt, Warren A., Jr.
Author_Institution :
Centaur Technol. Inc., Austin, TX, USA
Abstract :
We verify parts of the VIA Nano X86-compatible microprocessor design using the ACL2 theorem-proving system. We translate Nano RTL Verilog into the EMOD hardware description language. We specify properties of the Nano in the ACL2 logic and use a combination of theorem-proving and automated techniques to verify the correctness of Nano design elements.
Keywords :
hardware description languages; integrated circuit design; microprocessor chips; nanotechnology; theorem proving; ACL2 theorem-proving system; EMOD hardware description language; Nano RTL Verilog; VIA Nano X86-compatible microprocessor design; Equations; Hardware; Hardware design languages; Integrated circuit modeling; Logic gates; Mathematical model; Wire;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2010
Conference_Location :
Lugano
Print_ISBN :
978-1-4577-0734-6
Electronic_ISBN :
978-0-9835678-0-6
