论文标题
使用正式软件/硬件接口对加速器设计的应用程序级验证
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
论文作者
论文摘要
理想情况下,加速器开发应该与软件开发一样容易。最近的几种设计语言/工具正在实现此目标,但是由于建立专业编译器和模拟器支持的成本,实际上对端到端的实际应用测试早期设计仍然非常困难。我们提出了一种新的一流的,主要是自动化的方法,称为“ 3LA”,以实现未修改的源应用程序的原型加速器设计的端到端测试。 3LA的关键贡献是使用正式软件/硬件接口,该界面指定了加速器的操作及其语义。具体而言,我们利用指导级抽象(ILA)为加速器的正式规范,迄今已成功用于加速器实施验证。我们展示了加速器的ILA如何用作软件/硬件接口,类似于处理器的指令集体系结构(ISA),可用于编译器的自动开发和说明级模拟器。这项工作的另一个关键贡献是展示基于ILA基于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.