Leveraging Processor Modeling and Verification for General Hardware Modules

Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

For processors, an instruction-set-architecture (ISA) provides a complete functional specification that can be used to formally verify an implementation. There has been recent work in specifying accelerators using formal instruction sets, referred to as Instruction-Level Abstractions (ILAs), and using them to formally verify their implementations by leveraging processor verification techniques. In this paper, we generalize ILAs for specification of general hardware modules and formal verification of their RTL implementations. This includes automated generation of a complete set of functional (not including timing) specification properties using the ILA instructions. We address the challenges posed by this generalization and provide several case studies to demonstrate the applicability of this technique, including all the modules in an open-source 8051 micro-controller. This verification identified three bugs and completed in reasonable time.

Original languageEnglish (US)
Title of host publicationProceedings of the 2021 Design, Automation and Test in Europe, DATE 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1130-1135
Number of pages6
ISBN (Electronic)9783981926354
DOIs
StatePublished - Feb 1 2021
Event2021 Design, Automation and Test in Europe Conference and Exhibition, DATE 2021 - Virtual, Online
Duration: Feb 1 2021Feb 5 2021

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
Volume2021-February
ISSN (Print)1530-1591

Conference

Conference2021 Design, Automation and Test in Europe Conference and Exhibition, DATE 2021
CityVirtual, Online
Period2/1/212/5/21

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint

Dive into the research topics of 'Leveraging Processor Modeling and Verification for General Hardware Modules'. Together they form a unique fingerprint.

Cite this