pith. sign in

arxiv: 2606.13659 · v1 · pith:5QX5LGC5new · submitted 2026-06-11 · 💻 cs.PL · cs.AR

Specifying Hardware Communication as Programs

Ernest Ng , Nikil Shyamsunder , Francis Pham , Adrian Sampson , Kevin Laeufer This is my paper

Pith reviewed 2026-06-27 04:51 UTC · model grok-4.3

classification 💻 cs.PL cs.AR
keywords hardware communication protocolsdomain-specific languagedriver and monitorwaveform inferencetransaction-level tracehardware testingimperative specificationinterconnect protocols
0
0 comments X

The pith

A single imperative program in a DSL can specify hardware protocols for both driving designs and monitoring transactions.

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

Hardware modules are typically tested with two separate programs per protocol: a driver that turns high-level requests into pin signals and a monitor that reads signal traces back into transactions. Separate implementations create duplicated work and the chance that the two disagree on what the protocol allows. The paper instead defines a domain-specific language for writing one succinct imperative program that encodes the protocol once. The same program is then used in two ways: to generate the low-level interactions needed to drive a design under test, and as input to an inference procedure that, given a waveform, reconstructs the sequence of high-level transactions that occurred. If the approach holds, protocol authors would maintain only one artifact and could apply it directly to both stimulus generation and trace analysis on real interconnects such as Wishbone and AXI-Stream.

Core claim

The paper claims that hardware communication protocols can be expressed as succinct imperative programs inside a DSL, and that a single such program is sufficient both to drive a hardware module by emitting the required signal-level interactions and to monitor an execution by automatically inferring a consistent transaction-level trace from an observed waveform.

What carries the argument

The DSL of succinct imperative programs that describe protocol behavior, together with the inference procedure that, given the program and a waveform, produces a transaction trace consistent with both.

If this is right

  • Protocol authors maintain only one artifact instead of separate driver and monitor implementations.
  • The inference tool produces a transaction-level view directly from any waveform that matches the specification.
  • The same specification can be reused across design, test, and debug flows without manual translation.
  • Evaluation on Wishbone and AXI-Stream would show whether the DSL is expressive enough for production interconnect protocols.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The single-spec approach might allow the same program to serve as a reference model for formal equivalence checking between RTL implementations and the protocol definition.
  • If the inference procedure can be made efficient, it could be embedded inside existing waveform viewers to provide on-the-fly transaction annotations.
  • Extending the DSL with timing or power annotations could let the same program drive both functional and non-functional verification tasks.

Load-bearing premise

One succinct imperative program can encode all protocol rules needed for both driving and monitoring without forcing separate logic or leaving inconsistencies that the inference procedure cannot resolve.

What would settle it

Apply the inference tool to a waveform generated from a known correct transaction sequence on a protocol such as AXI-Stream; if the resulting inferred trace differs from the known sequence or the tool reports that no consistent trace exists, the central claim is falsified.

Figures

Figures reproduced from arXiv: 2606.13659 by Adrian Sampson, Ernest Ng, Francis Pham, Kevin Laeufer, Nikil Shyamsunder.

Figure 1
Figure 1. Figure 1: A ProtoLang protocol for a combinational adder. a memory controller and a waveform produced by its im￾plementation, the reconstructor will recognize instances of read and write transactions from the waveform and infer high-level parameters, such as the addresses and values for reads and writes. Using the reconstructor, users will be able to precisely verify whether their DUT’s behavior reflects their speci… view at source ↗
Figure 3
Figure 3. Figure 3: Multiple protocols defined over the same ALU. the receiver uses a ready bit to indicate that it is ready to consume data. The payload data is only transmitted during a clock cycle when ready and valid are both high. There are several rules associated with the ready-valid handshake, typically stated in prose (e.g., in the AXI-Stream specification [3]): • Independence: The sender cannot wait for ready to bec… view at source ↗
Figure 5
Figure 5. Figure 5: Two waveforms describing different scenarios that may occur during data transfer over a ready-valid interface. Left: receiver always asserts ready. Right: receiver exerts backpressure for one cycle [PITH_FULL_IMAGE:figures/full_fig_p004_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The ProtoLang interpreter takes as input multi￾ple user-defined protocols, a Verilog DUT implementation and a list of transactions to be executed, producing a wave￾form (signal-level execution trace) as output. controlling how step() and fork() interact with other lan￾guage features (§3.4, 3.5, 3.7) and detecting conflicting as￾signments between concurrent protocols (§3.6). As shown in figure 6, the interp… view at source ↗
Figure 7
Figure 7. Figure 7: The ProtoLang interpreter’s concurrent execution model, illustrated on the pipelined adder protocol ( [PITH_FULL_IMAGE:figures/full_fig_p006_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: An ill-formed protocol which invokes fork() with￾out previously calling step(). Rule: Protocols can fork() at most once. Another well￾formedness restriction governing the use of fork() is that a protocol can invoke fork() at most once in its body. If the same protocol were to call fork() twice within the same cycle, (i.e. fork(); fork(); ...), we would have two pro￾tocols beginning at the same time, violat… view at source ↗
Figure 9
Figure 9. Figure 9: Given an input ProtoLang specification and wave￾form for data transfer over a ready-valid interface, the re￾constructor infers a transaction trace consistent with the waveform. On waveforms that cannot be realized by the user-supplied specifications, the reconstructor reports an error. records the value of monitored signals at every clock cycle. These signals are visualized via waveform viewers, such as GT… view at source ↗
Figure 10
Figure 10. Figure 10: Example ProtoLang protocol specifications (top left) and waveform (top right) for a pipelined ALU. The different assignments for the op input port are highlighted in red. (Type annotations in the ProtoLang protocols are omitted for space.) Panels (a)–(e) illustrate how the reconstructor infers a transaction trace on this waveform. The resultant trace inferred by the reconstructor satisfies all constraints… view at source ↗
Figure 11
Figure 11. Figure 11: Example ProtoLang protocol (top left, abridged from [PITH_FULL_IMAGE:figures/full_fig_p012_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Simplified waveform illustrating the bug in the AXI-Stream FIFO implementation from Ma et al.’s dataset [28]. (e.g., separate channels for the data payload and target ad￾dress for reads and writes), and will require us to extend our language to describe dependencies between transactions on different channels. 6 Related Work SystemVerilog Assertions and UVM. SystemVerilog As￾sertions (SVA) [23] are a decla… view at source ↗
read the original abstract

To test and debug hardware modules, it is common to write two programs: a driver, which translates high-level transactions into interactions on the module's input and output signals, and a monitor, which analyzes a signal-level execution trace and recognizes a transaction. These two programs are commonly implemented separately for each hardware protocol, but this separation entails manual effort and risks inconsistencies. We advocate an alternative approach. We present a DSL in which users specify hardware communication protocols as succinct imperative programs. Crucially, the same specification can be used to both drive designs and monitor transactions. We present the design of a tool, which given a specification in our DSL and a waveform, automatically infers a transaction-level trace consistent with the waveform. We discuss plans to evaluate our DSL on real-world interconnects such as Wishbone and AXI-Stream.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 0 minor

Summary. The manuscript proposes a DSL in which hardware communication protocols are specified as succinct imperative programs. The central claim is that a single such specification can be used both to drive designs (translating high-level transactions to signal interactions) and to monitor transactions (via an automatic tool that infers a transaction-level trace from a waveform). The paper outlines the high-level design of the inference tool and states plans to evaluate the DSL on real-world interconnects such as Wishbone and AXI-Stream.

Significance. If the approach were realized with a consistent dual semantics and working inference procedure, it would address a genuine source of manual effort and inconsistency in hardware verification. However, the manuscript contains only an abstract-level design proposal with no examples, semantics, algorithm description, or evaluation results, so any significance remains prospective.

major comments (3)
  1. Abstract: the claim that 'the same specification can be used to both drive designs and monitor transactions' is presented without any formal semantics for the DSL, any description of the dual interpretation (generative vs. recognition), or any mechanism for ensuring consistency between the two modes. This is load-bearing for the central claim.
  2. Abstract: no worked example of even a simple protocol in the DSL is provided, nor any illustration of an inferred trace or how the inference tool would resolve nondeterminism. Without such concrete detail it is impossible to assess whether a single succinct program can faithfully serve both roles.
  3. Abstract: the inference tool is described only at the level of 'we present the design'; no algorithm, complexity argument, or handling of potential inconsistencies between driving and monitoring modes is supplied. This directly undermines the feasibility assertion in the reader's weakest assumption.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive feedback. We acknowledge that the current manuscript is a high-level proposal outlining the DSL concept and tool design without concrete examples or formal details, and we will revise the paper to incorporate the requested elements.

read point-by-point responses

  1. Referee: Abstract: the claim that 'the same specification can be used to both drive designs and monitor transactions' is presented without any formal semantics for the DSL, any description of the dual interpretation (generative vs. recognition), or any mechanism for ensuring consistency between the two modes. This is load-bearing for the central claim.

    Authors: We agree that formal semantics are necessary to support the central claim. The manuscript presents the idea at a conceptual level; in the revised version we will add a section defining the DSL semantics, specifying the generative interpretation for driving and the recognition interpretation for monitoring, and outlining how consistency between the two is maintained through a shared program representation. revision: yes

  2. Referee: Abstract: no worked example of even a simple protocol in the DSL is provided, nor any illustration of an inferred trace or how the inference tool would resolve nondeterminism. Without such concrete detail it is impossible to assess whether a single succinct program can faithfully serve both roles.

    Authors: We agree that the absence of a worked example limits assessment. The revised manuscript will include a simple protocol example (such as a basic handshake), showing the DSL program, its use for driving, a sample waveform, the inferred transaction trace, and how nondeterminism is resolved during inference. revision: yes

  3. Referee: Abstract: the inference tool is described only at the level of 'we present the design'; no algorithm, complexity argument, or handling of potential inconsistencies between driving and monitoring modes is supplied. This directly undermines the feasibility assertion in the reader's weakest assumption.

    Authors: We accept that the current description of the inference tool is high-level. In revision we will expand this section with an algorithm outline (including pseudocode), a complexity discussion, and explicit handling of nondeterminism and consistency with the driving semantics. revision: yes

Circularity Check

0 steps flagged

No circularity: design proposal with no derivations or fitted quantities

full rationale

The paper is a high-level design proposal for a DSL and inference tool. It contains no mathematical derivations, equations, predictions, fitted parameters, or uniqueness theorems. The central claim (one succinct program serving both driving and monitoring) is presented as a design goal without any self-referential reduction to its own inputs or self-citations that bear the load of a proof. No steps match any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review provides no equations, parameters, or entities; the proposal rests on the unstated assumption that an imperative DSL can unify driving and monitoring.

pith-pipeline@v0.9.1-grok · 5670 in / 979 out tokens · 27912 ms · 2026-06-27T04:51:33.587878+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

45 extracted references · 23 canonical work pages

  1. [1]

    Antmicro. 2022. Wishbone Interconnect Burst Mode Bench- mark.https://github.com/antmicro/wishbone-interconnect-burst- mode-benchmark

    2022

  2. [2]

    1999.AMBA Specification (Rev 2.0)

    ARM Limited. 1999.AMBA Specification (Rev 2.0). ARM Limited. https://developer.arm.com/documentation/ihi0011/latest/

    1999

  3. [3]

    2021.AMBA AXI-Stream Protocol Specification

    Arm Limited. 2021.AMBA AXI-Stream Protocol Specification. Arm Limited.https://developer.arm.com/documentation/ihi0051/latest/ Issue B, ID040921

    2021

  4. [4]

    2024.AMBA AXI and ACE Protocol Specification

    ARM Limited. 2024.AMBA AXI and ACE Protocol Specification. ARM Limited.https://developer.arm.com/documentation/ihi0022/latest/ Issue L

    2024

  5. [5]

    Jonathan Bachrach, Huy Vo, Brian Richards, Yunsup Lee, Andrew Waterman, Rimas Avižienis, John Wawrzynek, and Krste Asanović

  6. [6]

    Chisel: constructing hardware in a scala embedded language,

    Chisel: constructing hardware in a Scala embedded language. InProceedings of the 49th Annual Design Automation Conference(San Francisco, California)(DAC ’12). Association for Computing Machin- ery, New York, NY, USA, 1216–1225. doi:10.1145/2228360.2228584

    work page doi:10.1145/2228360.2228584

  7. [7]

    Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Deme- trescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques.ACM Comput. Surv.51, 3, Article 50 (2018)

    2018

  8. [8]

    Thomas Ball, Jakub Daniel, and Thomas Ball. 2015.Deconstructing Dynamic Symbolic Execution(proceedings of the 2014 marktoberdorf summer school on dependable software systems engineering, the 2014 marktober summer school on deop ed.). Technical Report MSR- TR-2015-95.https://www.microsoft.com/en-us/research/publication/ deconstructing-dynamic-symbolic-exec...

    2015

  9. [9]

    Griffin Berlstein, Rachit Nigam, Christophe Gyurgyik, and Adrian Sampson. 2023. Stepwise Debugging for Hardware Accelerators. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2023), Volume 2(Vancouver, BC, Canada). Association for Comput- ing Machinery, New York, NY, U...

    work page doi:10.1145/3575693 2023

  10. [10]

    Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind

  11. [11]

    InProceedings of the 41st ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(London, UK)(PLDI 2020)

    The essence of Bluespec: a core language for rule-based hardware design. InProceedings of the 41st ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing Machinery, New York, NY, USA, 243–257. doi:10.1145/3385412.3385965

    work page doi:10.1145/3385412.3385965 2020

  12. [12]

    Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, and Daw- son Engler. 2006. EXE: Automatically Generating Inputs of Death. InACM Conference on Computer and Communications Security (CCS 2006)(Alexandria, VA, USA). 322–335

    2006

  13. [13]

    Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later.Commun. ACM56, 2 (Feb. 2013), 82–90. doi:10.1145/2408776.2408795

    work page doi:10.1145/2408776.2408795 2013

  14. [14]

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

    work page doi:10.1109/43.945302 2001

  15. [15]

    Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification. In Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP). Association for Computing Machin- ery, New York, NY, USA, Article 24, ...

    work page doi:10.1145/3110268 2017

  16. [16]

    Lori A. Clarke. 1976. A Program Testing System. InThe ACM Annual Conference. doi:10.1145/800191.805647

    work page doi:10.1145/800191.805647 1976

  17. [17]

    cocotb contributors. 2021.cocotb: A coroutine based cosimulation library for writing VHDL and Verilog testbenches in Python.https: //github.com/cocotb/cocotbPython-based chip (RTL) verification framework

    2021

  18. [18]

    Stephen A. Cook. 1971. The complexity of theorem-proving pro- cedures. InProceedings of the Third Annual ACM Symposium on Theory of Computing(Shaker Heights, Ohio, USA)(STOC ’71). As- sociation for Computing Machinery, New York, NY, USA, 151–158. doi:10.1145/800157.805047

    work page doi:10.1145/800157.805047 1971

  19. [19]

    Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability modulo theories: introduction and applications.Commun. ACM54, 9 (Sept. 2011), 69–77. doi:10.1145/1995376.1995394

    work page doi:10.1145/1995376.1995394 2011

  20. [20]

    Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. InProgramming Language De- sign and Implementation (PLDI)(Chicago, IL, USA)(PLDI ’05). As- sociation for Computing Machinery, New York, NY, USA, 213–223. doi:10.1145/1065010.1065036

    work page doi:10.1145/1065010.1065036 2005

  21. [21]

    GTKWave contributors. [n. d.].GTKWave: A Fully Featured GTK+ Based Wave Viewer.https://gtkwave.sourceforge.netWaveform viewer for Unix, Win32, and Mac OSX supporting LXT, LXT2, VZT, FST, GHW, and Verilog VCD/EVCD files

  22. [22]

    2010.WISHBONE System-on-Chip (SoC) Inter- connection Architecture for Portable IP Cores

    Richard Herveille. 2010.WISHBONE System-on-Chip (SoC) Inter- connection Architecture for Portable IP Cores. OpenCores.https: //cdn.opencores.org/downloads/wbspec_b4.pdfRevision B.4

    2010

  23. [23]

    IEEE. 2020. IEEE Standard for Universal Verification Methodology Language Reference Manual.IEEE Std 1800.2-2020 (Revision of IEEE Std 1800.2-2017)(2020), 1–458. doi:10.1109/IEEESTD.2020.9195920

    work page doi:10.1109/ieeestd.2020.9195920 2020

  24. [25]

    IEEE. 2024. IEEE Standard for SystemVerilog–Unified Hardware De- sign, Specification, and Verification Language.IEEE Std 1800-2023 (Revision of IEEE Std 1800-2017)(2024), 1–1354. doi:10.1109/IEEESTD. 2024.10458102

    work page doi:10.1109/ieeestd 2024

  25. [26]

    James C. King. 1976. Symbolic execution and program testing.Com- mun. ACM19, 7 (July 1976), 385–394. doi:10.1145/360248.360252

    work page doi:10.1145/360248.360252 1976

  26. [27]

    Lucas Klemmer and Daniel Große. 2022. WAL: A Novel Waveform Analysis Language for Advanced Design Understanding and Debug- ging. InProceedings of the 27th Asia and South Pacific Design Automa- tion Conference(Taipei, Taiwan)(ASPDAC ’22). IEEE Press, 358–364. doi:10.1109/ASP-DAC52403.2022.9712600

    work page doi:10.1109/asp-dac52403.2022.9712600 2022

  27. [28]

    2024.Automated Testing, Verification and Repair of RTL Hardware Designs

    Kevin Laeufer. 2024.Automated Testing, Verification and Repair of RTL Hardware Designs. Ph. D. Dissertation. EECS Department, Uni- versity of California, Berkeley.http://www2.eecs.berkeley.edu/Pubs/ TechRpts/2024/EECS-2024-157.html

    2024

  28. [29]

    2021.chiseltest: The batteries-included testing and formal verification library for Chisel-based RTL designs

    Richard Lin and Kevin Laeufer. 2021.chiseltest: The batteries-included testing and formal verification library for Chisel-based RTL designs. https://github.com/ucb-bar/chiseltest

    2021

  29. [30]

    Jiacheng Ma, Gefei Zuo, Kevin Loughlin, Haoyang Zhang, Andrew Quinn, and Baris Kasikci. 2022. Debugging in the brave new world of reconfigurable hardware. InProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems(Lausanne, Switzerland)(ASPLOS ’22). Association for Computing Machinery, N...

    arXiv 2022

  30. [31]

    Peter Hofstee, and Zaid Al-Ars

    Raffaele Meloni, H. Peter Hofstee, and Zaid Al-Ars. 2024. In2024 IEEE Nordic Circuits and Systems Conference (NorCAS). 1–6. doi:10.1109/ NorCAS64408.2024.10752465

    arXiv 2024

  31. [32]

    Rachit Nigam. 2026. Defining Safe Hardware Design. Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE). Co-located with ASPLOS ’26

    2026

  32. [33]

    Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson. 2023. Modular Hardware Design with Timeline Types. InProceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Vol. 7. Association for Computing Machinery, New York, NY, USA, Article 120, 25 pages. doi:10.1145/3591234

    work page doi:10.1145/3591234 2023

  33. [34]

    Rachit Nigam, Ethan Gabizon, Edmund Lam, Carolyn Zech, Jonathan Balkind, and Adrian Sampson. 2026. Parameterized Hardware Design with Latency-Abstract Interfaces. InASPLOS ’26: 31st ACM Interna- tional Conference on Architectural Support for Programming Languages and Operating Systems. doi:10.1145/3779212.3790199

    work page doi:10.1145/3779212.3790199 2026

  34. [35]

    Rishiyur Nikhil. 2004. Bluespec System Verilog: efficient, correct RTL from high level specifications. InProceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE ’04). IEEE Computer Society, USA, 69–70. doi:10.1109/ MEMCOD.2004.1459818

    arXiv 2004

  35. [36]

    Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, and Adam Chlipala. 2021. Effective simulation and debugging for a high-level hardware language using software compilers. InProceedings of the 26th ACM International Conference on Architectural Support for Pro- gramming Languages and Operating Systems (ASPLOS ’21). Asso- ciation for Computing Machin...

    work page doi:10.1145/3445814.3446720 2021

  36. [37]

    Amir Pnueli. 1977. The temporal logic of programs. In18th Annual Symposium on Foundations of Computer Science (SFCS 1977). doi:10. 1109/sfcs.1977.32

    1977

  37. [38]

    Andrew Ray. 2020. Using ASCII Waveforms to Test Hardware De- signs.https://blog.janestreet.com/using-ascii-waveforms-to-test- hardware-designs/. Published on the Jane Street Technology Blog

    2020

  38. [39]

    Andy Ray, Benjamin Devlin, Fu Yong Quah, and Rahul Yesantharao

  39. [40]

    InProceedings of the 2024 ACM/SIGDA International Symposium on Field Programmable Gate Arrays(Mon- terey, CA, USA)(FPGA ’24)

    Hardcaml: An OCaml Hardware Domain-Specific Language for Efficient and Robust Design. InProceedings of the 2024 ACM/SIGDA International Symposium on Field Programmable Gate Arrays(Mon- terey, CA, USA)(FPGA ’24). Association for Computing Machinery, New York, NY, USA, 41. doi:10.1145/3626202.3637586

    work page doi:10.1145/3626202.3637586 2024

  40. [41]

    Katharina Ruep and Daniel Große. 2022. SpinalFuzz: Coverage-Guided Fuzzing for SpinalHDL Designs. In2022 IEEE European Test Symposium (ETS). 1–4. doi:10.1109/ETS54262.2022.9810421 15 Ernest Ng, Nikil Shyamsunder, Francis Pham, Adrian Sampson, and Kevin Laeufer

    work page doi:10.1109/ets54262.2022.9810421 2022

  41. [42]

    Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, and Klaus Wehrle. 2020. Symbolic Partial-Order Execution for Testing Multi-Threaded Programs. InComputer Aided Verification (CA V) 2020 (Los Angeles, CA, USA). Springer-Verlag, Berlin, Heidelberg, 376–400. doi:10.1007/978-3-030-53288-8_18

    work page doi:10.1007/978-3-030-53288-8_18 2020

  42. [43]

    Koushik Sen and Gul Agha. 2006. CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. InComputer Aided Verification (CA V)(Seattle, WA)(CA V’06). Springer-Verlag, Berlin, Hei- delberg, 419–423. doi:10.1007/11817963_38

    work page doi:10.1007/11817963_38 2006

  43. [44]

    Frans Skarman, Lucas Klemmer, Daniel Große, Oscar Gustafsson, and Kevin Laeufer. 2025. Surfer — An Extensible Waveform Viewer. In Computer Aided Verification: 37th International Conference, CA V 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV(Zagreb, Croatia). Springer-Verlag, Berlin, Heidelberg, 392–404. doi:10.1007/978-3-031- 98685-7_19

    work page doi:10.1007/978-3-031- 2025

  44. [45]

    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. InASPLOS ’26: 31st ACM Interna- tional Conference on Architectural Support for Programming Languages and Operating Systems. doi:10.1145/3779212.3790125

    work page doi:10.1145/3779212.3790125 2026

  45. [46]

    2022.Source-Level Debugging for Hardware Generator Frameworks

    Keyi Zhang. 2022.Source-Level Debugging for Hardware Generator Frameworks. Ph. D. Dissertation. Stanford University. 16

    2022