The Essence of Bluespec: A Core Language for Rule-Based Hardware Design

Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind. The Essence of Bluespec: A Core Language for Rule-Based Hardware Design. Proceedings of the ACM SIGPLAN 2020 Conference on Programming Language Design and Implementation (PLDI'20). June 2020.

Paper as PDF

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 Kôika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Kôika 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.

GitHub repository