Reference. Modular Hardware Design with Timeline Types

Rachit Nigam, Pedro H. Azevedo de Amorim, Adrian Sampson · PLDI · 2023 · hardware type-systems · PDF · DOI · pldb
Modular design is a key challenge for enabling large-scale reuse of hardware modules. Unlike software, however, hardware designs correspond to physical circuits and inherit constraints from them. Timing constraints—which cycle a signal arrives, when an input is read—and structural constraints—how often a multiplier accepts new inputs—are fundamental to hardware interfaces. Existing hardware design languages do not provide a way to encode these constraints; a user must read documentation, build scripts, or in the worst case, a module’s implementation to understand how to use it. We present Filament, a language for modular hardware design that supports the specification and enforcement of timing and structural constraints for statically scheduled pipelines. Filament uses timeline types, which describe the intervals of clock-cycle time when a given signal is available or required. Filament enables safe composition of hardware modules, ensures that the resulting designs are correctly pipelined, and predictably lowers them to efficient hardware.

Cite
Cite as @nigam_amorim_sampson_2023 (helia, typst) · \cite{nigam_amorim_sampson_2023} (LaTeX)
BibTeX
bibtex · 12 lines
@article{nigam_amorim_sampson_2023,
 title = {Modular Hardware Design with Timeline Types},
 author = {Nigam, Rachit and Amorim, Pedro H. Azevedo de and Sampson, Adrian},
 year = {2023},
 doi = {10.1145/3591234},
 url = {https://dl.acm.org/doi/abs/10.1145/3591234},
 publisher = {ACM},
 journal = {Proceedings of the ACM on Programming Languages},
 volume = {7},
 number = {PLDI},
 pages = {343--367}
}
hayagriva YAML (typst)
yaml · 18 lines
nigam_amorim_sampson_2023:
  type: article
  title: Modular Hardware Design with Timeline Types
  author:
  - Nigam, Rachit
  - Amorim, Pedro H. Azevedo de
  - Sampson, Adrian
  date: 2023
  page-range: 343-367
  url: https://dl.acm.org/doi/abs/10.1145/3591234
  serial-number:
    doi: 10.1145/3591234
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: ACM
    issue: PLDI
    volume: 7
Download: nigam_amorim_sampson_2023.bib · nigam_amorim_sampson_2023.yml
Cited by (2)

Parameterized Hardware Design with Latency-Abstract Interfaces nigam-2026-parameterizedASPLOS · 2026
DOI

Unifying Static and Dynamic Intermediate Languages for Accelerator Generators kim-2024-unifyingOOPSLA · 2024
Compilers for accelerator design languages (ADLs) translate high-level languages into application-specific hardware. ADL compilers rely on a hardware control interface to compose hardware units. There are two choices: static control, which relies on cycle-level timing; or dynamic control, which uses explicit signalling to avoid depending on timing details. Static control is efficient but brittle; dynamic control incurs hardware costs to support compositional reasoning. Piezo is an ADL compiler that unifies static and dynamic control in a single intermediate language (IL). Its key insight is that the IL’s static fragment is a refinement of its dynamic fragment: static code admits a subset of the run-time behaviors of the dynamic equivalent. Piezo can optimize code by combining facts from static and dynamic submodules, and it opportunistically converts code from dynamic to static control styles. We implement Piezo as an extension to an existing dynamic ADL compiler, Calyx. We use Piezo to implement a frontend for an existing ADL, a systolic array generator, and a packet-scheduling hardware generator to demonstrate its optimizations and the static–dynamic interactions it enables.
PDF · DOI · arXiv · pldb
Cites 54 works (3 here)
With notes (3)

A compiler infrastructure for accelerator generators nigam-2021-aASPLOS · 2021
DOI · arXiv

Predictable accelerator design with time-sensitive affine types nigam-2020-predictablePLDI · 2020
PDF · DOI · arXiv · pldb

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002
In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
DOI
External (51)
nigam_amorim_sampson_2023 reference entries/refs/nigam_amorim_sampson_2023/nigam_amorim_sampson_2023.hel