Anvil: A General-Purpose Timing-Safe Hardware Description Language
Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, Prateek Saxena
Abstract
Expressing hardware designs using hardware description languages (HDLs) routinely involves using stateless signals whose values change according to their underlying registers. Unintended behaviours can arise when the stored values in these underlying registers are mutated while their dependent signals are expected to remain constant across multiple cycles. Such timing hazards are common because, with a few exceptions, existing HDLs lack abstractions for values that remain unchanged over multiple clock cycles, delegating this responsibility to hardware designers. Designers must then carefully decide whether a value should remain unchanged, sometimes even across hardware modules. This paper proposes Anvil, an HDL which statically prevents timing hazards with a novel type system. Anvil is the only HDL we know of that guarantees timing safety, i.e., absence of timing hazards, without sacrificing expressiveness for cyclelevel timing control or dynamic timing behaviours. Unlike many HLS languages that abstract away the differences between registers and signals, Anvil's type system exposes them fully while capturing the timing relationships between register value mutations and signal usages to enforce timing safety. This, in turn, enables safe composition of communicating hardware modules by static enforcement of timing contracts that encode timing constraints on shared signals. Such timing contracts can be specified parametric on abstract time points that can vary during run-time, allowing the type system to statically express dynamic timing behaviour. We have implemented Anvil and successfully used it to implement key timing-sensitive modules, comparing them against open-source SystemVerilog counterparts to demonstrate the practicality and expressiveness of the generated hardware.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext a120c24a-6b2d-40b9-aa26-e38cb794e43dCited by top-tier papers1
Ask how each one uses itBuilds on8
- The essence of Bluespec: a core language for rule-based hardware designThomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, ArvindPLDI 2020 · 55 citations
- Modular Hardware Design with Timeline TypesRachit Nigam, Pedro Henrique Azevedo de Amorim, Adrian SampsonPLDI 2023 · 16 citations
- Wire sorts: a language abstraction for safe hardware compositionMichael Christensen, Timothy Sherwood, Jonathan Balkind, Ben HardekopfPLDI 2021 · 13 citations
- HIR: An MLIR-based Intermediate Representation for Hardware Accelerator DescriptionKingshuk Majumder, Uday BondhugulaASPLOS 2023 · 12 citations
- PDL: a high-level hardware design language for pipelined processorsDrew Zagieboylo, Charles Sherk, Gookwon Edward Suh, Andrew C. MyersPLDI 2022 · 9 citations
Related papers
- HyperFlow: A Processor Architecture for Nonmalleable, Timing-Safe Information Flow SecurityAndrew Ferraiuolo, Mark Zhao, Andrew C. Myers, G. Edward SuhCCS 2018 · 63 citations
- VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow PropertiesArmaiti Ardeshiricham, Yoshiki Takashima, Sicun Gao, Ryan KastnerCCS 2019 · 19 citations
- Predictable accelerator design with time-sensitive affine typesRachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li et al.PLDI 2020 · 58 citations
- Modular Hardware Design of Pipelined Circuits with HazardsMinseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao et al.PLDI 2024 · 4 citations
- Unifying Static and Dynamic Intermediate Languages for Accelerator GeneratorsCaleb Kim, Pai Li, Anshuman Mohan, Andrew Butt et al.OOPSLA 2024 · 1 citation
