The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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.
@article{subramanyan2017templatebased,
title = {Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification},
author = {Pramod Subramanyan and Bo-Yuan Huang and Yakir Vizel and Aarti Gupta and Sharad Malik},
year = {2017},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
publisher = {Institute of Electrical and Electronics Engineers},
volume = {37},
number = {8},
pages = {1692--1705},
doi = {10.1109/tcad.2017.2764482},
}