Anvil: A General-Purpose Timing-Safe Hardware Description Language
Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, Prateek Saxena
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper1
问问它们各自怎么用它它引用的顶会 Paper8
- The essence of Bluespec: a core language for rule-based hardware designThomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, ArvindPLDI 2020 · 被引用 55 次
- Modular Hardware Design with Timeline TypesRachit Nigam, Pedro Henrique Azevedo de Amorim, Adrian SampsonPLDI 2023 · 被引用 16 次
- Wire sorts: a language abstraction for safe hardware compositionMichael Christensen, Timothy Sherwood, Jonathan Balkind, Ben HardekopfPLDI 2021 · 被引用 13 次
- HIR: An MLIR-based Intermediate Representation for Hardware Accelerator DescriptionKingshuk Majumder, Uday BondhugulaASPLOS 2023 · 被引用 12 次
- PDL: a high-level hardware design language for pipelined processorsDrew Zagieboylo, Charles Sherk, Gookwon Edward Suh, Andrew C. MyersPLDI 2022 · 被引用 9 次
相关 Paper
- HyperFlow: A Processor Architecture for Nonmalleable, Timing-Safe Information Flow SecurityAndrew Ferraiuolo, Mark Zhao, Andrew C. Myers, G. Edward SuhCCS 2018 · 被引用 63 次
- VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow PropertiesArmaiti Ardeshiricham, Yoshiki Takashima, Sicun Gao, Ryan KastnerCCS 2019 · 被引用 19 次
- Predictable accelerator design with time-sensitive affine typesRachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li 等PLDI 2020 · 被引用 58 次
- Modular Hardware Design of Pipelined Circuits with HazardsMinseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao 等PLDI 2024 · 被引用 4 次
- Unifying Static and Dynamic Intermediate Languages for Accelerator GeneratorsCaleb Kim, Pai Li, Anshuman Mohan, Andrew Butt 等OOPSLA 2024 · 被引用 1 次
