Hardware design should be SAFER!
Memory-safe software languages changed the world and allowed to us to build massively larger systems. At their heart, memory-safe languages eliminate a category of bugs that pointer-manipulating programs suffer from.
Hardware design needs its own safe programming models but instead of memory, the problem is time! Synchronous hardware design needs to deal with a clock signal which creates discrete time steps. Every hardware module needs to think about how time affects its own logic and everything it communicates with. Getting it wrong leads to all sorts of logical bugs: reading meaningless values and using resources that are unavailable.
Our work on Filament (https://filamentHDL.com) defined a criteria for safe hardware description languages (HDLs) and showed that you can enforce it using a type system and introduce no overheads. Safe HDLs have become an interesting area of research and this year's ASPLOS features two papers exploring different threads:
- Lilac (https://arxiv.org/abs/2401.02570): Builds upon Filament applies its safety guarantees to parameterized designs. A cool outcome of this work was to show that, in addition to helping with verification, safe HDLs enable the design of fundamentally new abstractions!
- Anvil (https://arxiv.org/abs/2503.19447): Explores how Filament's verification abstractions can be applied to a higher-level, message-passing HDL and enforce safety properties!
I'm really excited to see where this line of work goes and what we can build with it! If you're around at ASPLOS and interested in this kind of work, come say hi and go watch the talks!!
Mastodon Feed
