Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification
Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification
复制标题
用于 SoC 验证的统一指令级抽象的基于模板的参数化综合
DOI：
--
复制
发表时间：
2018
影响因子：
2.9
通讯作者：
S. Malik
中科院分区：
文献类型：
--
作者：
P. Subramanyan;Bo;Y. Vizel;Aarti Gupta;S. Malik
现代片上系统（SoC）设计包括可编程内核、专用加速器和I/O设备。加速器由软件/固件控制，功能由可编程内核、固件和加速器的组合实现。这种SoC的验证是具有挑战性的，特别是对于由固件和硬件的组合维护的系统级属性。尝试用固件和硬件正式验证完整的SoC设计是不可扩展的，而单独的验证可能会遗漏错误。可扩展系统级验证的一种通用技术是构造SoC硬件的抽象并使用其验证固件/软件。构造抽象来捕获所需的细节和交互是容易出错且耗时的。第二个是确保抽象的正确性，以便用它证明的属性是有效的。提出了一种基于层次抽象综合的SoC设计与验证方法。ILA是SoC硬件的抽象，其以指令的粒度对固件可见状态的更新进行建模。对于硬件加速器，ILA类似于用于可编程处理器的配置集架构定义，并且实现与硬件加速器交互的固件的可扩展验证。为了减轻手工构造抽象的缺点，我们介绍了两种算法的合成ILAs从部分描述称为模板。然后，我们将展示如何ILA可以被验证为正确的。我们评估的方法，使用一个小的SoC设计组成的8051微控制器和两个加密加速器。该方法发现了15个bug。
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.