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 \emph{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.