• DocumentCode
    545645
  • Title

    Verifying VIA Nano microprocessor components

  • Author

    Hunt, Warren A., Jr.

  • Author_Institution
    Centaur Technol. Inc., Austin, TX, USA
  • fYear
    2010
  • fDate
    20-23 Oct. 2010
  • Firstpage
    3
  • Lastpage
    10
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • 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
  • Type

    conf

  • Filename
    5770925
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=545645