Abstract
High-level synthesis (HLS) seeks to make hardware development more like software development by adapting ideas from programming languages to hardware description and HLS from functional languages is usually motivated as a means of bringing software-like productivity to hardware development. Formalized semantics support a range of important capabilities in software languages (e.g., compositionality, comprehensibility, interoperability, formal methods, and security) that are desirable in hardware languages as well. This paper considers the formalized semantics of the Device Calculus, a typed lambda-calculus with operators for constructing Mealy machines that forms a semantic substratum suitable for high-level synthesis and we demonstrate the utility of the Device Calculus as a foundation for formal methods in functional HLS with a case study specifying the semantics of an idealized subset of the FIRRTL language. FIRRTL (``Flexible Internal Representation for RTL'') is an open-source hardware intermediate representation targeted by the Chisel hardware construction language and the semantics we present is also a starting point for exploring formal methods and security within both the Chisel toolchain and any other high-level synthesis flows that target FIRRTL.
| Original language | English |
|---|---|
| Title of host publication | 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021) |
| DOIs | |
| State | Published - Oct 2021 |
| Externally published | Yes |
Fingerprint
Dive into the research topics of 'A Mechanized Semantic Metalanguage for High Level Synthesis'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver