Skip to main content

Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification

Author(s): Subramanyan, Pramod; Huang, Bo-Yuan; Vizel, Yakir; Gupta, Aarti; Malik, Sharad

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1nc1v
Full metadata record
DC FieldValueLanguage
dc.contributor.authorSubramanyan, Pramod-
dc.contributor.authorHuang, Bo-Yuan-
dc.contributor.authorVizel, Yakir-
dc.contributor.authorGupta, Aarti-
dc.contributor.authorMalik, Sharad-
dc.date.accessioned2021-10-08T19:46:53Z-
dc.date.available2021-10-08T19:46:53Z-
dc.date.issued2017-10en_US
dc.identifier.citationSubramanyan, Pramod, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, and Sharad Malik. "Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification." IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, no. 8 (2017): pp. 1692-1705. doi:10.1109/TCAD.2017.2764482en_US
dc.identifier.issn0278-0070-
dc.identifier.urihttps://cse.iitk.ac.in/users/spramod/papers/tcad17.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1nc1v-
dc.description.abstractModern system-on-chip (SoC) designs comprise programmable cores, application-specific accelerators, and I/O devices. Accelerators are controlled by software/firmware and functionality is implemented by this combination of programmable cores, firmware, and accelerators. Verification of such SoCs is challenging, especially for system-level properties maintained by a combination of firmware and hardware. Attempting to formally verify the full SoC design with both firmware and hardware is not scalable, while separate verification can miss bugs. A general technique for scalable system-level verification is to construct an abstraction of SoC hardware and verify firmware/software using it. There are two challenges in applying this technique in practice. Constructing the abstraction to capture required details and interactions is error-prone and time-consuming. The second is ensuring abstraction correctness so that properties proven with it are valid. This paper introduces a methodology for SoC design and verification based on the synthesis of instruction-level abstractions (ILAs). The ILA is an abstraction of SoC hardware which models updates to firmware-visible state at the granularity of instructions. For hardware accelerators, the ILA is analogous to the instruction-set architecture definition for programmable processors and enables scalable verification of firmware interacting with hardware accelerators. To alleviate the disadvantages of manual construction of abstractions, we introduce two algorithms for synthesis of ILAs from partial description called templates. We then show how the ILA can be verified to be correct. We evaluate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 15 bugs.en_US
dc.format.extent1692 - 1705en_US
dc.language.isoen_USen_US
dc.relation.ispartofIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systemsen_US
dc.rightsAuthor's manuscripten_US
dc.titleTemplate-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verificationen_US
dc.typeJournal Articleen_US
dc.identifier.doi10.1109/TCAD.2017.2764482-
dc.identifier.eissn1937-4151-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/journal-articleen_US

Files in This Item:
File Description SizeFormat 
TemplateInstructLevelAbstractionsSocVerif.pdf507.22 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.