Pith. sign in

REVIEW 3 major objections 3 minor 41 references

High-Level Synthesis of Efficient Pipelines with Visibility Control

T0 review · 3 major / 3 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Fine-grained pipelining control and sequential semantics can coexist in high-level synthesis.

desk verdict A genuine new abstraction and strong PPA numbers, but the main RISC-V design relies on an optimization the refinement proof never covers. read the letter →

arxiv 2607.18765 v1 pith:SHC7QKLJ submitted 2026-07-21 cs.PL cs.AR

Jungin Rhee , Minseong Jang , Jaewoo Kim , Jeehoon Kang This is my paper · ORCID
classification cs.PLcs.AR
keywords high-levelsynthesispipelininghazardresolutionsequentialsemanticsvisibilitycontrolspeculationregisterrenaminghardwaredesign
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that the traditional trade-off in high-level synthesis—between fine-grained control over a pipeline's structure and hazard resolution on one side, and the safety of sequential program semantics on the other—is not inherent. The authors present an HLS tool built on 'visibility control,' an abstraction in which each in-flight loop iteration publishes its pending reads and writes to shared state in stages, and later iterations react to what is visible. Stalling, bypassing, speculation, deferred commit, and register renaming all become instances of this single mechanism, selectable per variable and per access. Because the source program remains sequential, the compiled pipeline is claimed to refine it; because a compiler specializes each hazard-resolution network to the chosen strategy, the resulting designs are claimed to match hand-written RTL in power, performance, and area. A sympathetic reader would care because it promises to make hardware design-space exploration as easy as editing sequential code while keeping the performance of custom RTL.

What carries the argument

The central object is the Var wrapper type and its published-state machines: each token carries S_decl (whether it will store), a batch of store slots that advance through Declared, Tentative, and Sealed states, plus S_load and S_spec for loads and speculative reads. The rules of Fig. 3 determine whether a later token stalls, forwards, or reads the base state. The compiler's two analyses—program-order analysis and state-reachability analysis—are what make the abstraction efficient rather than merely expressive.

What would settle it

Search for a counterexample by random generation: loops satisfying the four eager-commit conditions, compiled with the optimization enabled, simulated cycle-by-cycle, and compared against the sequential execution of the same Rust program. A single mismatch in base-state values after loop completion (or after any read) would falsify the refinement claim.

Watch

Extended reading notes

Core claim

The central claim, on the paper's own terms, is that visibility control unifies hazard resolution: every strategy is a pair of choices about what an earlier instruction exposes of its pending stores and loads on shared state, and how a later instruction reacts. The paper instantiates this in a Rust-based sequential language with a Var type whose load, spec_load, try_load, and staged write protocol (declare/store/seal/drop) mirror the published-state machines. It then shows that a compiler can map these operations to efficient hardware: a program-order analysis decides most token orderings statically, and a state-reachability analysis prunes published-state components to fixed wires and bypas

Load-bearing premise

The load-bearing premise is that the eager tentative commit optimization—which writes tentative values directly into shared storage before an iteration's commit point—is sound; the paper states four conditions for it but provides no proof that it preserves the refinement from source to pipeline.

Editorial extensions

If this is right

  • If correct, hardware designers can explore pipeline strategies by small, local edits (moving or deleting declare/store/seal operations) without re-verifying concurrency.
  • The same sequential source can be compiled to stall, bypass, speculative, or renaming pipelines, making design-space exploration a compiler-level knob rather than an RTL rewrite.
  • Hazard resolution can be specialized per variable and per address, including per-address speculation, which prior rule-based approaches could not express.
  • The two static analyses imply that for many pipelines (e.g., a 5-stage CPU) all program-order comparisons are decided at compile time, eliminating runtime comparators and loop-index registers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The visibility-control lens suggests a taxonomy: hazard resolution strategies are really scheduling of when side effects become observable; this may transfer to out-of-order cores or multi-core memory consistency, which the paper leaves as future work.
  • If the eager tentative commit optimization is proven sound and the four conditions are sufficient, it may generalize to more than one eager Var per loop via grouped flushes, an extension the paper does not claim.
  • The paper's refinement proof is sketched and, as the paper itself acknowledges in the appendix, does not cover the eager tentative commit optimization; readers should treat the correctness guarantee for that optimization as open.
  • The per-address speculation mechanism (S_spec) could be reused as a building block for memory disambiguation in software-pipelined loops targeting FPGAs.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. This paper presents an HLS tool that embeds fine-grained pipeline-structure and hazard-resolution control in a sequential Rust-like programming model. The key idea is visibility control: each instruction publishes its pending reads/writes through Var and SpecVar, and hazard-resolution strategies (stall, bypass, speculation, deferred commit, register renaming) are expressed by the placement of publish/observe operations. The authors formalize a token-based operational semantics of the target pipeline (Figs. 13–15), sketch a refinement proof that the pipeline's committed base-state updates are permitted by the source program (§5.3), and describe compiler analyses (program-order and state-reachability) that specialize the generated hardware. They evaluate on 5-stage RISC-V cores, countif histograms, and an AES accelerator, reporting PPA comparable to hand-written RTL and better than sequential-semantics HLS baselines. An artifact provides pre-built compiler binaries, case-study sources, and evaluation scripts.

Significance. If the claims hold, this is a strong systems contribution: a single abstraction unifying several hazard-resolution mechanisms under sequential semantics, with an evaluation spanning CPU, memory-bound, and control-heavy designs. The operational semantics is a useful formal foundation, and the program-order analysis (which eliminates comparators and loop indices for the RISC-V case) is elegant. The empirical comparison to PDL, Vitis HLS, Dynamatic, Sodor, and Kanagawa is valuable, and the artifact is a concrete reproducibility effort. The proof is explicitly informal, and no machine-checked compiler correctness is claimed. However, the central correctness guarantee is not currently established for the headline RISC-V PC configuration because the eager tentative-commit optimization used there is outside the formal semantics and the proof sketch. Closing this gap, or explicitly rescoping the correctness claim, is necessary before the paper's central 'sequential semantics with fine-grained control' statement is fully supported.

major comments (3)
  1. [§5.3 / §C.2] The refinement proof in §5.3 proves property 3 (base-storage value matches source) from the Drop-Ok rule in Fig. 15, which is the only rule that writes to Σ. Appendix C.2's eager tentative commit writes Tentative values into base storage on store, before the token's commit point, and replaces later spec_loads with base reads. No such rule appears in Fig. 15, so the formal semantics does not cover the optimization; the induction property 3 cannot be derived. The four conditions in C.2 are asserted, not proved; condition 2 is intra-token (read-before-write within one token) and does not by itself establish the inter-token invariant that a flushed token's eager write is overwritten before a non-flushed read, nor that the final base state equals the sequential result. Since §6.2 states the 5-stage CPU's pc uses this optimization, the claim [[Π]]Pipe ⊑ [[S]]Rust is unproven for the headline d
  2. [Fig. 15 / §5.2] The formal visibility-operation rules omit spec_load and try_load, although §4.2 presents them as part of the Var API and §5.2 describes spec_load in prose (try_load is mentioned as a non-blocking variant). The proof sketch in §5.3 explicitly depends on spec_load's Sspec record ('Speculative loads fit the same induction because Sspec records every address read speculatively'). With no SpecLoad/TryLoad rules, the semantics does not define these operations, so the refinement statement for the speculative examples (Fig. 2e and Fig. 7's pc) is not formally grounded. Please add the missing rules or explicitly restrict the formal development to conservative loads.
  3. [§5.3 vs §C.1] The proof is a sketch over an abstract Π obtained by a structural mapping; it does not state a theorem connecting the actual MIR/SIR→Verilog compiler to Π. In addition, Appendix A.6 discloses that the compiler source is not shipped, only pre-built binaries. Hence the 'compiled pipeline refines source' claim is not independently checkable at the compiler level. The paper should scope the claim explicitly (e.g., 'for pipelines produced by the intended mapping') and, if feasible, include compiler sources or a validated extraction. This is a standard limitation for proof sketches, but given the centrality of the correctness claim it should be stated.
minor comments (3)
  1. [Table 4] The rows for 'Ours' and 'Ours Opt' appear to have been merged or corrupted in the typeset table: two sets of numbers and ratios are interleaved in a single row. Please reformat so each configuration has its own row and units are clear.
  2. [Running header] The running header on page 2 reads '2 Trovato et al.'; this appears to be a template leftover and should be corrected to match the paper's authors or removed.
  3. [§5.3] The proof sketch refers to 'liveΠc(T)' and a non-liveness mechanism for speculative tokens, but this predicate is not defined in Figs. 12–15. The informal description in §5.2 helps, but a precise definition would make the proof easier to check.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claims are measured against external baselines, and the formal refinement is an independent theorem about a defined transition system, not an input to its own derivation.

full rationale

The paper's central claims are system-construction and evaluation claims, not derivations. The PPA/CPI claims are validated against external baselines (PDL [42], Sodor [4], Vitis HLS [23], Dynamatic [22], Kanagawa [30]), none of which are the authors' work, and no parameter is fitted to these benchmarks; the reported numbers are simulation and synthesis measurements, so there is no fitted-input-called-prediction step. The formal claim [[Π]]Pipe ⊑ [[S]]Rust (§5.3) is not self-definitional: [[S]]Rust is the independent ordinary-Rust semantics of the source, and [[Π]]Pipe is a transition system defined by the rules of Figures 13-15; the proof sketch derives the refinement from those rules rather than assuming it. The load-bearing external dependency is PDL's structural loop-to-pipeline mapping (§4.1, 'We adopt PDL's structural mapping'), which is external prior work by other authors and is extended, not relied upon as a black-box guarantee of the paper's own correctness. The only self-citations ([17] ShakeFlow, [19] Jang et al., and the anonymous supplemental [2]) appear in the related-work survey of §8 and the artifact appendix, not as evidence for the correctness or PPA claims, so there is no load-bearing self-citation and no uniqueness/ansatz smuggled in via self-citation. The manuscript itself flags genuine limitations that I weigh here: §5.3 is explicitly an 'informal correctness proof sketch,' §8 states 'Future work. We are mechanizing the proof sketch of §5,' and the Eager Tentative Commit optimization of §C.2 is supported only by four asserted conditions with an informal argument, yet §6.2 states the predicted PC 'is written to pc's storage register by an eager tentative commit,' so the headline RISC-V design's refinement is not covered by the §5.3 induction as written. This is a real correctness risk — an omitted proof — but it is not circularity: the refinement claim is not an input to the derivation, and an unproven or even unsound optimization would be a soundness failure, not a case where the result is equivalent to its inputs by construction. Per the scoring rubric, the honest finding is no-significant-circularity, with the proof gap recorded as a correctness concern rather than a reduction of the paper's claims to their own premises.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

No free parameters are fitted to evaluation data; hardware parameters (stage boundaries, BHT size) are design choices. The proof relies on the token abstraction, Rust type-system enforcement, and an informal induction.

assumptions (4)
  • domain assumption The token abstraction and latency-insensitive valid-ready protocol accurately model the target hardware pipeline.
    The formal pipeline semantics in §5.1–5.2 is built on token flow with valid-ready handshakes, citing Carloni et al. [6]; the correctness argument assumes this model is faithful.
  • domain assumption Rust's ownership/typestate system correctly enforces that every StoreBatch commits exactly once in the allowed order.
    The staged write protocol in §4.2 relies on RAII and mutable borrowing; the source-language constraints are assumed to be sound and the compiler to preserve them.
  • domain assumption Lexicographic program order over loop indices is a total order that matches the hardware's in-order issue/exit behavior.
    The program-order analysis in §6.1 and the correctness sketch in §5.3 use this ordering; the in-order branch join and break flush rules in Fig. 14 are assumed to enforce it.
  • domain assumption The informal simultaneous induction over loop iterations in §5.3 is valid for every program in the supported Rust subset.
    The paper gives a proof sketch, not a machine-checked proof; the authors state in §8 that they are mechanizing it.
invented entities (2)
  • Var<T,N> independent evidence
    purpose: A wrapper type that instantiates visibility control on a shared array, exposing declare/store/seal/drop operations and load/spec_load/try_load to resolve dependency hazards.
    Implemented in the compiler artifact and used across all three case studies; its behavior is formally specified in Fig. 15.
  • SpecVar<T> independent evidence
    purpose: A wrapper for advisory state whose load returns arbitrary values and store is a no-op, compiled to hazard-free shared storage (e.g., branch history table).
    Implemented in the compiler and used in the RISC-V dynamic branch prediction design.

how reviews work

0 comments
Cite this review

Pith. "Pith review of High-Level Synthesis of Efficient Pipelines with Visibility Control." pith.science (2026). https://pith.science/paper/SHC7QKLJ

@misc{pith2026260718765,
  author       = {Pith},
  title        = {Pith review of: High-Level Synthesis of Efficient Pipelines with Visibility Control},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SHC7QKLJ}},
  note         = {Machine review of arXiv:2607.18765}
}
read the original abstract

High-level synthesis (HLS) raises the abstraction of hardware design from concurrent register-transfer level (RTL) programs to sequential programs. Among the forms of parallelism HLS exploits, pipelining demands fine-grained control over pipeline structure and hazard resolution to achieve competitive power, performance, and area (PPA). However, existing tools either lack such control or sacrifice sequential semantics to provide it. We present an HLS tool that embeds fine-grained pipeline control in a sequential programming model, enabling rapid design-space exploration. The tool builds on visibility control, a novel programming abstraction that unifies hazard resolution strategies including stalling, bypassing, speculation, deferred commit, and register renaming. We evaluate on in-order RISC-V cores, histograms, and an AES accelerator. On RISC-V cores, we implement stall, bypass, speculation, and register renaming; on histograms, we implement scheduling strategies that previously required RTL or concurrent programming models. Compiled pipelines outperform HLS tools with sequential semantics and achieve PPA comparable to hand-written RTL.

Figures

Figures reproduced from arXiv: 2607.18765 by the authors.

Figure 1
Figure 1. PDL’s programming model: the datapath program (a) and the resulting CPU structure (b). [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Dependency hazard resolution in pipelined CPUs, viewed through the lens of visibility control. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. An instruction’s action for each operation, given an earlier instruction’s published state. Symbols: [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (14 more)
Figure 4
Figure 4. Figure 4: Compilation of a loop with a conditional two-stage adder. [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: Source-level API of Var. issues every subtoken speculatively, PDL’s call issues the successor token only after its arguments are resolved. Speculative issue instead requires spec_call, which bundles it with value speculation on the arguments. Second, whereas the loop s…
Figure 6
Figure 6. Figure 6: States and transitions for 𝑆batch (a list of slots, each an independent 𝑆store) and 𝑆spec (addresses read by spec_load). deviating program does not compile: (1) a StoreBatch mutably borrows its Var ( [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: 5-stage pipelined CPU code with bypass and static prediction. [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 9
Figure 9. Figure 9: Hardware-module instantiation of [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: Register renaming with try_load. return None and are skipped instead of stalling the scan, while a free register returns Some(true) and is selected (L10–13). Once a physical register is allocated, the free list (L14–21) and the rename table (L23–26) are updated, and a…
Figure 11
Figure 11. Figure 11: Dynamic prediction with SpecVar. 𝑥, 𝑦 ∈ 𝐿𝑜𝑐𝑎𝑙𝑉 𝑎𝑟 𝑋, 𝑌 ∈ 𝑉 𝑎𝑟 𝑎 ∈ 𝐴𝑑𝑑𝑟 𝑣 ∈ 𝑉 𝑎𝑙𝑢𝑒 𝑛 ∈ N 𝑒 ∈ Combinational 𝑟 ∈ 𝑆𝑙𝑜𝑡𝑆𝑡𝑎𝑡𝑒 ::= Declared(𝑎) | Tentative(𝑎, 𝑣) | Sealed(𝑎, 𝑣 ? ) 𝑆pub ∈ 𝑃𝑢𝑏𝑙𝑖𝑠ℎ𝑒𝑑𝑆𝑡𝑎𝑡𝑒 ::= (𝑆decl, 𝑆batch, 𝑆load, 𝑆spec) 𝑃𝑉 ∈ 𝑃𝑢𝑏𝑙𝑖𝑠ℎ𝑒𝑑𝑉𝑖𝑒𝑤 ::= 𝑉 𝑎𝑟 ⇀ 𝑆pub 𝐿 ∈ L…
Figure 12
Figure 12. Figure 12: Type definitions for pipeline states. 𝐴 → 𝐵 denotes a total function, and 𝐴 ⇀ 𝐵 denotes a partial function. Given a partial function 𝑓 , 𝑓 [𝑎 ↦→ 𝑏] denotes the function that maps 𝑎 to 𝑏 and behaves as 𝑓 elsewhere. 5.1 Pipeline State in Tokens [PITH_FULL_IMAGE:figures…
Figure 13
Figure 13. Figure 13: Core rules for the cycle-level transition relation. [PITH_FULL_IMAGE:figures/full_fig_p017_13.png]
Figure 14
Figure 14. Figure 14: Loop-control rules for the cycle-level transition relation. [PITH_FULL_IMAGE:figures/full_fig_p018_14.png]
Figure 15
Figure 15. Figure 15: Visibility-operation rules for Var. conflicting store to an address recorded in 𝑆spec makes the speculative token non-live through liveΠc (𝑇 ), preventing it from reaching an irreversible drop. 5.3 Correctness Proof Sketch We provide an informal correctness proof sket…
Figure 16
Figure 16. Figure 16: Tokens and the program order encoded by their loop indices. [PITH_FULL_IMAGE:figures/full_fig_p020_16.png]
Figure 17
Figure 17. Figure 17: Compile-time specialization of [PITH_FULL_IMAGE:figures/full_fig_p022_17.png]
Figure 18
Figure 18. Figure 18: PDL code with a WAW hazard and its execution trace, with the unsound rule set fails to reject. [PITH_FULL_IMAGE:figures/full_fig_p032_18.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 1 canonical work pages

  1. [1]

    AMD. [n. d.]. Vitis High-Level Synthesis User Guide (UG1399): Pipeline. https://docs.amd.com/r/en-US/ug1399-vitis- hls/Pipeline

  2. [2]

    Anonymous Author(s). 2026. Supplemental Materials for This Submission

    2026

  3. [3]

    Jonathan Bachrach, Huy Vo, Brian Richards, Yunsup Lee, Andrew Waterman, Rimas Avižienis, John Wawrzynek, and Krste Asanović. 2012. Chisel: constructing hardware in a Scala embedded language. InProceedings of the 49th Annual Design Automation Conference(San Francisco, California)(DAC ’12). Association for Computing Machinery, New York, NY, USA, 1216–1225. ...

    arXiv 2012

  4. [4]

    Berkeley Architecture Research. 2021. Sodor Core. https://github.com/ucb-bar/riscv-sodor/tree/sodor-old

    2021

  5. [6]

    Carloni, K.L

    L.P. Carloni, K.L. McMillan, and A.L. Sangiovanni-Vincentelli. 2001. Theory of latency-insensitive design.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems20, 9 (2001), 1059–1076. doi:10.1109/43.945302

    doi:10.1109/43.945302 2001

  6. [7]

    2018.A Highly Productive Implementation of an Out-of-Order Processor Generator

    Christopher Celio. 2018.A Highly Productive Implementation of an Out-of-Order Processor Generator. Ph. D. Dissertation. EECS Department, University of California, Berkeley. http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS- 2018-151.html

    2018

  7. [8]

    Hongzheng Chen, Niansong Zhang, Shaojie Xiang, Zhichen Zeng, Mengjia Dai, and Zhiru Zhang. 2024. Allo: A Programming Model for Composable Accelerator Design.Proc. ACM Program. Lang.8, PLDI, Article 171 (June 2024), 28 pages. doi:10.1145/3656401

    work page doi:10.1145/3656401 2024

  8. [9]

    Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification.Proc. ACM Program. Lang.1, ICFP, Article 24 (aug 2017), 30 pages. doi:10.1145/3110268

    doi:10.1145/3110268 2017

Show all 41 references
  1. [10]

    John Clow, Georgios Tzimpragos, Deeksha Dangwal, Sammy Guo, Joseph McMahan, and Timothy Sherwood. 2017. A pythonic approach for rapid hardware prototyping and instrumentation. In2017 27th International Conference on Field Programmable Logic and Applications (FPL). 1–7. doi:10....

    2017

  2. [12]

    Embedded Microprocessor Benchmark Consortium. 2023. EEMBC. https://www.eembc.org/

    2023

  3. [13]

    Snoeren, George Porter, and George Papen

    Alex Forencich, Alex C. Snoeren, George Porter, and George Papen. 2020. Corundum: An Open-Source 100-Gbps Nic. In2020 IEEE 28th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 38–46. doi:10.1109/FCCM48280.2020.00015

    2020

  4. [14]

    Hasan Genc, Seah Kim, Alon Amid, Ameer Haj-Ali, Vighnesh Iyer, Pranav Prakash, Jerry Zhao, Daniel Grubb, Harrison Liew, Howard Mao, Albert Ou, Colin Schmidt, Samuel Steffl, John Wright, Ion Stoica, Jonathan Ragan-Kelley, Krste Asanovic, Borivoje Nikolic, and Yakun Sophia Shao....

    2021 arXiv

  5. [15]

    Google. 2025. XLS: Accelerated HW Synthesis. https://github.com/google/xls/blob/main/docs_src/scheduling.md# minimizing-pipeline-registers-via-sdc-scheduling-sdc. 27

    2025

  6. [16]

    Jean-Michel Gorius, Simon Rokicki, and Steven Derrien. 2022. SpecHLS: Speculative Accelerator Design Using High-Level Synthesis.IEEE Micro42, 5 (2022), 99–107. doi:10.1109/MM.2022.3188136

    2022

  7. [17]

    Sungsoo Han, Minseong Jang, and Jeehoon Kang. 2023. ShakeFlow: Functional Hardware Description with Latency- Insensitive Interface Combinators. InProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volu...

    2023

  8. [18]

    Janestreet. 2025. hardcaml. https://github.com/janestreet/hardcaml Accessed: 2025-07-05

    2025

  9. [19]

    Minseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao, and Jeehoon Kang. 2024. Modular Hardware Design of Pipelined Circuits with Hazards.Proc. ACM Program. Lang.8, PLDI, Article 148 (June 2024), 24 pages. doi:10.1145/ 3656378

    2024

  10. [20]

    Lana Josipovic, Philip Brisk, and Paolo Ienne. 2017. An Out-of-Order Load-Store Queue for Spatial Computing.ACM Trans. Embed. Comput. Syst.16, 5s, Article 125 (Sept. 2017), 19 pages. doi:10.1145/3126525

    2017 doi

  11. [21]

    Lana Josipovic, Andrea Guerrieri, and Paolo Ienne. 2019. Speculative Dataflow Circuits. InProceedings of the 2019 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays(Seaside, CA, USA)(FPGA ’19). Association for Computing Machinery, New York, NY, USA, 162–171. d...

    2019

  12. [22]

    Lana Josipović, Andrea Guerrieri, and Paolo Ienne. 2022. From C/C++ Code to High-Performance Dataflow Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems41, 7 (2022), 2142–2155. doi:10.1109/ TCAD.2021.3105574

    2022

  13. [23]

    Vinod Kathail. 2020. Xilinx Vitis Unified Software Platform. InProceedings of the 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays(Seaside, CA, USA)(FPGA ’20). Association for Computing Machinery, New York, NY, USA, 173–174. doi:10.1145/3373087.3375887

    2020

  14. [24]

    David Koeplinger, Matthew Feldman, Raghu Prabhakar, Yaqi Zhang, Stefan Hadjis, Ruben Fiszel, Tian Zhao, Luigi Nardi, Ardavan Pedram, Christos Kozyrakis, and Kunle Olukotun. 2018. Spatial: a language and compiler for application accelerators. InProceedings of the 39th ACM SIGPL...

    2018

  15. [25]

    Dario Korolija, Timothy Roscoe, and Gustavo Alonso. 2020. Do OS abstractions make sense on FPGAs?. In14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 991–1010. https://www.usenix.org/conference/osdi20/presentation/roscoe

    2020

  16. [26]

    Nicholas Matsakis. 2015. RFC 1211: Mid-level IR (MIR). Rust RFC Repository. https://rust-lang.github.io/rfcs/1211- mir.html Accessed: 2026-04-13

    2015

  17. [27]

    Rachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li, Theodore Bauer, Yuwei Ye, Apurva Koti, Adrian Sampson, and Zhiru Zhang. 2020. Predictable accelerator design with time-sensitive affine types. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language D...

    2020

  18. [28]

    Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson. 2023. Modular Hardware Design with Timeline Types.Proc. ACM Program. Lang.7, PLDI, Article 120 (June 2023), 25 pages. doi:10.1145/3591234

    2023 doi

  19. [29]

    R. Nikhil. 2004. Bluespec System Verilog: efficient, correct RTL from high level specifications. InProceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE ’04.69–70. doi:10.1109/MEMCOD.2004.1459818

    2004 arXiv

  20. [30]

    Blake Pelton, Adam Sapek, Ken Eguro, Daniel Lo, Alessandro Forin, Matt Humphrey, Jinwen Xi, David Cox, Rajas Karandikar, Johannes de Fine Licht, Evgeny Babin, Adrian Caulfield, and Doug Burger. 2024. Wavefront Threading Enables Effective High-Level Synthesis.Proc. ACM Program....

    2024

  21. [31]

    Brandon Reagen, Robert Adolf, Yakun Sophia Shao, Gu-Yeon Wei, and David Brooks. 2014. MachSuite: Benchmarks for accelerator design and customized architectures. In2014 IEEE International Symposium on Workload Characterization (IISWC). 110–119. doi:10.1109/IISWC.2014.6983050

    2014

  22. [32]

    SecWorks. 2025. AES (Advanced Encryption Standard) Library. https://github.com/secworks/aes. Accessed: 2025-07-08

    2025

  23. [33]

    Siemens EDA. 2025. Catapult High-Level Synthesis and Verification. https://eda.sw.siemens.com/en-US/ic/catapult- high-level-synthesis/. Accessed: 2025-07-05

    2025

  24. [34]

    Wilson Snyder. 2024. Verilator. https://www.veripool.org/verilator/

    2024

  25. [35]

    Synopsys, Inc. [n. d.].Design Compiler RTL Synthesis Solution. https://www.synopsys.com/implementation-and- signoff/rtl-synthesis-test/dc-ultra.html Accessed: 2025-07-08

    2025

  26. [36]

    The MLIR Authors. 2026. MLIR: ’scf’ Dialect (Structured Control Flow). https://mlir.llvm.org/docs/Dialects/SCFDialect/. Accessed: 2026-04-13

    2026

  27. [37]

    Vinay Vashishtha, Manoj Vangala, and Lawrence T. Clark. 2017. ASAP7 predictive design kit development and cell design technology co-optimization: Invited paper. In2017 IEEE/ACM International Conference on Computer-Aided 28 Trovato et al. Design (ICCAD). 992–998. doi:10.1109/IC...

    2017

  28. [38]

    Myers, and G

    Yulun Yao, Drew Zagieboylo, Andrew C. Myers, and G. Edward Suh. 2025. Sequential Specifications for Precise Hardware Exceptions. InProceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1(USA)(ASPLO...

    2025

  29. [39]

    Hanchen Ye, Cong Hao, Jianyi Cheng, Hyunmin Jeong, Jack Huang, Stephen Neuendorffer, and Deming Chen. 2022. ScaleHLS: A New Scalable High-Level Synthesis Framework on Multi-Level Intermediate Representation. In2022 IEEE International Symposium on High-Performance Computer Arch...

    2022

  30. [40]

    Hanchen Ye, Hyegang Jun, and Deming Chen. 2024. HIDA: A Hierarchical Dataflow Compiler for High-Level Synthesis. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1(La Jolla, CA, USA)(ASPLOS ...

    2024

  31. [41]

    Carlson, and Prateek Saxena

    Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, and Prateek Saxena. 2026. Anvil: A General-Purpose Timing-Safe Hardware Description Language. InProceedings of the 31st ACM International Conference on Architectural Support for Programming Languages an...

    2026

  32. [42]

    Drew Zagieboylo, Charles Sherk, Gookwon Edward Suh, and Andrew C. Myers. 2022. PDL: A High-Level Hardware Design Language for Pipelined Processors. InProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation(San Diego, CA, U...

    2022

  33. [43]

    in-order stages

    F. Zaruba and L. Benini. 2019. The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology.IEEE Transactions on Very Large Scale Integration (VLSI) Systems27, 11 (Nov 2019), 2629–2640. doi:10.1...

    2019

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.