|
|
|
|
LEADER |
02051 am a22002293u 4500 |
001 |
131094.2 |
042 |
|
|
|a dc
|
100 |
1 |
0 |
|a Bourgeat, Thomas
|e author
|
100 |
1 |
0 |
|a Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
|e contributor
|
100 |
1 |
0 |
|a Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science
|e contributor
|
700 |
1 |
0 |
|a Pit-Claudel, Clément
|e author
|
700 |
1 |
0 |
|a Chlipala, Adam
|e author
|
700 |
1 |
0 |
|a Arvind, Arvind
|e author
|
245 |
0 |
0 |
|a The essence of Bluespec: a core language for rule-based hardware design
|
260 |
|
|
|b Association for Computing Machinery (ACM),
|c 2021-09-23T19:07:11Z.
|
856 |
|
|
|z Get fulltext
|u https://hdl.handle.net/1721.1/131094.2
|
520 |
|
|
|a The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits. Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design. In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies. Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits. We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.
|
520 |
|
|
|a Defense Advanced Research Projects Agency (DARPA) (Grant CCF-1521584)
|
520 |
|
|
|a National Science Foundation (Grant HR001118C0018)
|
546 |
|
|
|a en
|
655 |
7 |
|
|a Article
|
773 |
|
|
|t PLDI 2020: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
|