使用形式化软硬件接口的加速器设计应用级验证
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
AI总结：
针对早期加速器设计端到端测试成本过高的问题，提出名为3LA的自动化方法，基于ILA形式化软硬件接口实现编译器与模拟器自动生成，仅需少量工程投入即可完成验证，还曾发现并助力修复已发表加速器的未知缺陷。
摘要：
理想情况下，加速器开发应像软件开发一样简便。近期已有多种设计语言/工具朝这一目标推进，但由于构建专用编译器和模拟器支持的成本过高，在真实应用上对早期设计进行端到端测试目前仍难度极大、难以实现。我们提出了一种首创的、基本自动化的全新方法，名为“3LA”，可在未经修改的原始应用上对原型加速器设计开展端到端测试。3LA的一项核心贡献是采用了一种形式化软硬件接口，该接口定义了加速器的操作及其语义。具体而言，我们利用了加速器的指令级抽象（Instruction-Level Abstraction，ILA）形式化规范，该规范此前已成功应用于加速器实现验证。我们展示了加速器的ILA如何作为软硬件接口（类似于处理器的指令集架构（Instruction Set Architecture，ISA）），可用于编译器和指令级模拟器的自动化开发。本研究的另一项关键贡献是，证明了基于ILA的加速器语义如何能够拓展近期在等式饱和方面的研究成果，通过我们称为“灵活匹配”的技术，为原型加速器自动生成基础编译器支持。将灵活匹配与由ILA规范自动生成的模拟器相结合，我们的方法仅需少量工程投入即可实现端到端评估。我们详细介绍了3LA的多个案例研究，该方法在一款近期发表的加速器中发现了一处未知缺陷，并助力完成了缺陷修复。
英文摘要：
Ideally, accelerator development should be as easy as software development. Several recent design languages/tools are working toward this goal, but actually testing early designs on real applications end-to-end remains prohibitively difficult due to the costs of building specialized compiler and simulator support. We propose a new first-in-class, mostly automated methodology termed "3LA" to enable end-to-end testing of prototype accelerator designs on unmodified source applications. A key contribution of 3LA is the use of a formal software/hardware interface that specifies an accelerator's operations and their semantics. Specifically, we leverage the Instruction-Level Abstraction (ILA) formal specification for accelerators that has been successfully used thus far for accelerator implementation verification. We show how the ILA for accelerators serves as a software/hardware interface, similar to the Instruction Set Architecture (ISA) for processors, that can be used for automated development of compilers and instruction-level simulators. Another key contribution of this work is to show how ILA-based accelerator semantics enables extending recent work on equality saturation to auto-generate basic compiler support for prototype accelerators in a technique we term "flexible matching." By combining flexible matching with simulators auto-generated from ILA specifications, our approach enables end-to-end evaluation with modest engineering effort. We detail several case studies of 3LA, which uncovered an unknown flaw in a recently published accelerator and facilitated its fix.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
