A general purpose language for safer, yet expressive hardware design.
Try Anvil · Documentation · Research paper · Pact · Community
Anvil is a general-purpose hardware description language (HDL) that gives designers control over registers and clock-cycle latency. Its type system ensures that values are used only while valid and that registers are not overwritten while still in use. This property is called timing safety and is enforced at compile time.
Pact extends Anvil with session types for communication between components. Each component declares an interface whose type describes its communication behaviour, control flow, and timing. The compiler checks that every process conforms to its declared type and that the types of processes composed together are compatible. Compatible processes exchange messages synchronously without deadlocking. This property is called communication safety and is enforced at compile time.
Pact can also check compatibility in an open setting, where some components are not yet available. This allows designers to build large systems incrementally.
Anvil and Pact designs compile to synthesizable SystemVerilog.
| Timing safety | Communication safety | RTL expressiveness | Hardware efficiency |
|---|---|---|---|
| Anvil's type system enforces timing safety modularly. | Pact's session types ensure that composed components never deadlock and keep making progress. | Designers control registers and cycle-level latency. | Anvil designs add no clock-cycle latency and have minimal overhead in area, power, and frequency. Pact designs also add no clock-cycle latency. |
Run a program in the online playground, work through the tutorial, or install the compiler. The language reference covers syntax and semantics.
- Anvil compiler — The compiler, tests, and example hardware designs.
- Language server — Experimental language support and editor extensions for VS Code and Vim/Neovim.
- Documentation — The source for the documentation site, tutorial, and language reference.
- Evaluation experiments — Evaluation designs, test harnesses, synthesis reports, and reproduction instructions.
- RISCy experiment — A simple pipelined RISC-V processor written in Anvil.
- Pact compiler — Anvil extended with session types and compatibility checking.
- Pact experiments — Pact benchmarks, SystemVerilog references, and the scripts for the POPL 2027 evaluation.
- Pact formalization — The Lean 4 mechanization of Pact's type system.
-
Aditya Ranjan Jha, Jason Zhijingcheng Yu, Umang Mathur, and Prateek Saxena. 2027. A Type System for Communication Safe Hardware Design. Proceedings of the ACM on Programming Languages (POPL 2027). To appear.
-
Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, and Prateek Saxena. 2026. Anvil: A General-Purpose Timing-Safe Hardware Description Language. In Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’26). Association for Computing Machinery. DOI: 10.1145/3779212.3790125.
For discussions please join AnvilHDL Zulip community. Report bugs or propose changes through the compiler, Pact compiler, language server, or documentation issue trackers. Contributions are welcome.
For collaborations or queries, please reach out to one of the maintainers:
