Semi-Automated Translation of a Formal ISA Specification to Hardware

on YouTube ↗09m

" summary

Prototype pipeline converts Sail ISA specs into Clash hardware by translating Sail’s monadic effects into monadic stream functions that compile to a naive single‑cycle RISC‑V subset implementation. The pipeline composes state/exception/nondeterminism monads into effect‑parameterized arrows, generates functional finite‑state transducers, and emits Verilog via Clash; it works end‑to‑end on a subset of RISC‑V as a proof‑of‑concept and aims to add microarchitectural effects (timing, resources) for refined multi‑cycle designs.

AI-written summary · about

" chapters (8)

1. 0:00Intro
2. 0:13Overview
3. 1:43Sail for Formal ISA Specification
4. 3:17CASH for Hardware Design
5. 4:41Composition is Hard
6. 5:41Monadic Stream Functions
7. 6:54User's Perspective
8. 7:23Bridging the Chasm and Then Some

" related talks

• 36mTowards a Formally-verified Software Toolchain for open ISAsBoris Shingarov · OpenPOWER Summit NA 2020
• 02h 49mA Tour of the RISC V ISA Formal SpecificationRishiyur Nikhil · RISC-V Summit 2019
• 26mArchSem: Reusable Rigorous Semantics of Relaxed ArchitecturesPeter Sewell, Zongyuan Liu, Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Nils Lauermann, Alasdair Armstrong · POPL 2026
• 20mSail RISC-V: Status and Future ChallengesAlasdair Armstrong · RISC-V Summit North America 2024
• 59mTutorial: High Level Sail OverviewBill McSpadden · RISC-V Summit 2022
• 31mFormal SpecificationThomas Bourgeat · 8th RISC-V Workshop Barcelona 2018
• 27mClash: Haskell as an HDLMartijn Bastiaan · ORConf 2018
• 09mDemo: RISC-V Instruction Information Parsing and Storage for SAILPaul Clarke · RISC-V Summit North America 2023