[Session 1] Towards Gradually Typed Hardware Description Languages

[zsisco]

Authors: Peitian Pan, Shunning Jiang, Yanghui Ou, Christopher Batten (Cornell University)
https://capra.cs.cornell.edu/latte23/paper/12.pdf

[sampsyo]

I think this paper's classifying perspective on embedded HDLs is really seriously useful. To paraphrase the paper, Chisel is statically typed (because Scala is) and PyMTL is dynamically typed (because Python is). To state the obvious, the actual hardware being generated remains statically typed! It's just the generator that enjoys static or dynamic typing, and there are real consequences to either choice.

There is a very interesting effect here where, to bring dynamically-typed generation into a statically-typed world, you can do post-elaboration checking. You can check that the generated hardware actually conforms to the type you were hoping for. Simulation-time type checking is a little more straightforward (it looks like ordinary "dynamic typing" for ordinary CPU languages).

One question I'd be interested in hearing about from the entire LATTE audience: what has your experience been with dynamic- or statically-typed embedded HDLs? Have you been frustrated by the static type system in something like Chisel, or have you been burned by the flexibility of a dynamic generator in a Python-embedded HDL?