Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface

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 sim...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-08
Main Authors: Bo-Yuan, Huang, Lyubomirsky, Steven, Li, Yi, He, Mike, Smith, Gus Henry, Tambe, Thierry, Gaonkar, Akash, Canumalla, Vishal, Cheung, Andrew, Gu-Yeon, Wei, Gupta, Aarti, Tatlock, Zachary, Malik, Sharad
Format: Article
Language:English
Subjects:
Accelerators
Applications programs
Compilers
Deep learning
Domain specific languages
Hardware
Image processing
Machine learning
Portability
Prototypes
Semantics
Software
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422