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

To refer to this page use:
Abstract: Modern 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.
Publication Date: Oct-2017
Citation: Subramanyan, 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.2764482
DOI: 10.1109/TCAD.2017.2764482
ISSN: 0278-0070
EISSN: 1937-4151
Pages: 1692 - 1705
Type of Material: Journal Article
Journal/Proceeding Title: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Version: Author's manuscript

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