Template-based synthesis of instruction-level abstractions for SoC verification

Pramod Subramanyan, Yakir Vizel, Sayak Ray, Sharad Malik

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

16 Scopus citations

Abstract

Contemporary integrated circuits are complex system-on-chip (SoC) designs consisting of programmable cores along with accelerators and peripherals controlled by firmware running on the cores. The functionality of the SoC is implemented by a combination of firmware and hardware components. As a result, verifying these two components separately can miss bugs while attempting to formally verify the full SoC design considering both firmware and hardware is not scalable. An abstraction that can be used instead of the cycle-Accurate and bit-precise hardware implementation can be helpful in scalably verifying system-level properties of SoCs. However, constructing such an abstraction to capture all the required details and interactions is error-prone, tedious and time-consuming. Another challenge is ensuring correctness of the abstraction so that properties proven using it are valid. In this paper, we introduce a methodology for SoC verification. We synthesize an instruction-level abstraction (ILA) that precisely captures updates to all firmware-Accessible states spanning the cores, accelerators and peripherals. The synthesis algorithm uses a blackbox simulator to synthesize the ILA from a template specification. A golden-model generated from the ILA is used to verify whether the hardware implementation matches the ILA. We demonstrate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 14 bugs.

Original languageEnglish (US)
Title of host publicationProceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
EditorsRoope Kaivola, Thomas Wahl
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages160-167
Number of pages8
ISBN (Electronic)9780983567851
DOIs
StatePublished - Aug 11 2016
Event15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 - Austin, United States
Duration: Sep 27 2015Sep 30 2015

Publication series

NameProceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015

Other

Other15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
CountryUnited States
CityAustin
Period9/27/159/30/15

All Science Journal Classification (ASJC) codes

  • Engineering (miscellaneous)
  • Computer Science Applications
  • Software

Fingerprint Dive into the research topics of 'Template-based synthesis of instruction-level abstractions for SoC verification'. Together they form a unique fingerprint.

  • Cite this

    Subramanyan, P., Vizel, Y., Ray, S., & Malik, S. (2016). Template-based synthesis of instruction-level abstractions for SoC verification. In R. Kaivola, & T. Wahl (Eds.), Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 (pp. 160-167). [7542266] (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/FMCAD.2015.7542266