Arch: An AI-Native Hardware Description Language for Register-Transfer Clocked Hardware Design

Shuqing Zhao

arxiv: 2604.05983 · v3 · submitted 2026-04-07 · 💻 cs.PL · cs.CL

Arch: An AI-Native Hardware Description Language for Register-Transfer Clocked Hardware Design

Shuqing Zhao This is my paper

Pith reviewed 2026-05-10 18:28 UTC · model grok-4.3

classification 💻 cs.PL cs.CL

keywords hardware description languageAI code generationregister transfer leveltype safetyclock domain crossingSystemVerilogformal verification

0 comments

The pith

Arch is a hardware description language that uses parameterized types for clocks and resets to enforce safety rules at compile time and is designed for easy generation by AI models.

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

The paper introduces Arch, a new language for describing register-transfer level hardware that is optimized for both human readability and AI code generation. It treats clocks and resets as typed parameters rather than simple signals, which allows the compiler to automatically check for issues like improper clock domain crossings and invalid data patterns. Arch also provides built-in support for common hardware components such as pipelines, state machines, and FIFOs instead of requiring users to implement them manually in error-prone ways. This approach aims to make hardware design more reliable and accessible to AI assistance by ensuring the syntax is simple and predictable for large language models. If the design works as intended, it could lead to fewer bugs in complex digital circuits generated with the help of AI.

Core claim

Arch provides first-class constructs for pipelines, FSMs, FIFOs, arbiters, register files, buses with handshake channels, clock-domain crossings, and multi-cycle threads. Clocks and resets are parameterized types (Clock<D>, Reset<S,P,D?>) rather than ordinary nets, converting CDC and reset-domain analysis from external linter passes into compile-time typing rules. The language follows an AI-generatability contract with an LL(1) grammar, no preprocessor, uniform declaration schema, named block endings, and a todo! escape hatch to allow LLMs to produce structurally correct, type-safe code from natural-language specifications without fine-tuning. The compiler emits SystemVerilog and generates

What carries the argument

Parameterized types for clocks and resets that integrate domain crossing and reset analysis into the type system, combined with first-class constructs for micro-architectural elements and an LL(1) grammar to support AI generation.

Load-bearing premise

That the specific syntactic choices in Arch, including its LL(1) grammar and uniform structure, will allow large language models to reliably generate correct and type-safe hardware code from natural language descriptions without any model fine-tuning.

What would settle it

Running an experiment where an off-the-shelf LLM is prompted to describe a design involving clock domain crossing in Arch and checking if the generated code violates the claimed type safety or contains structural errors.

read the original abstract

We present Arch (AI-native Register-transfer Clocked Hardware), a hardware description language for micro-architecture specification and AI-assisted code generation. Arch provides first-class constructs for pipelines, FSMs, FIFOs, arbiters, register files, buses with handshake channels, clock-domain crossings, and multi-cycle threads -- structures that existing HDLs express only as user-defined patterns prone to subtle errors. A central design choice is that clocks and resets are parameterized types (Clock<D>, Reset<S,P,D?>) rather than ordinary nets, converting CDC and reset-domain analysis from external linter passes into compile-time typing rules. Bit widths, port directions, single-driver ownership, and combinational acyclicity are tracked in the same pass, catching latches, width mismatches, loops, and unsynchronized crossings before simulation. A guard clause on reg declarations captures the valid-data pattern declaratively, catching the producer bug where a valid flag asserts before data is written. Every syntactic choice is governed by an AI-generatability contract: an LL(1) grammar, no preprocessor, a uniform declaration schema, named block endings, and a todo! escape hatch let LLMs produce structurally correct, type-safe Arch from natural-language specs without fine-tuning. The compiler emits lint-clean IEEE 1800-2017 SystemVerilog and auto-generates safety properties (FIFO no-overflow, counter range, FSM legal-state, handshake protocol) verified with Verilator -- assert and EBMC, plus direct AST-to-SMT-LIB2 bounded model checking via arch formal. An integrated simulator compiles designs to native C++ with Python cocotb support. Case studies: L1 cache and AXI DMA (Yosys/OpenSTA, Sky130); 428/431 tests pass on VerilogEval and CVDP.

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.

Desk Editor's Note private letter to a colleague

Arch adds compile-time type checks for clocks, resets, and hardware patterns that catch real errors, but its AI-native claim has no supporting LLM experiments.

read the letter

Arch's main advance is making clocks and resets into parameterized types instead of plain wires. That turns CDC and reset-domain problems into type errors the compiler catches before simulation. The language also gives first-class syntax for pipelines, FIFOs, arbiters, and the valid-data guard on registers, so those patterns stop being error-prone user idioms. The compiler emits clean SystemVerilog, auto-generates safety properties for FIFOs and FSMs, and includes a cocotb-backed simulator. The L1 cache and AXI DMA case studies plus the 428/431 pass rate on VerilogEval and CVDP show the type rules and backend actually work on realistic designs. That part is concrete and useful. The soft spot is the AI-generatability contract. The authors chose an LL(1) grammar, no preprocessor, uniform declarations, and named block ends so LLMs can supposedly emit correct code from specs without fine-tuning. They present this as a direct consequence of the syntax, yet the paper contains no prompting trials, error rates, or head-to-head comparisons with Verilog or Chisel. All reported results come from hand-written code or standard benchmarks, not from model output. The central positioning therefore rests on an untested hypothesis. This paper is for hardware language designers and people building AI-assisted EDA flows. The typing and verification pieces are solid enough that a serious editor should send it to peer review, though the AI angle will need experiments to hold up.

Referee Report

2 major / 1 minor

Summary. The manuscript introduces Arch, an AI-native hardware description language for register-transfer clocked hardware design. It provides first-class constructs for pipelines, FSMs, FIFOs, arbiters, register files, buses with handshake channels, clock-domain crossings, and multi-cycle threads. Clocks and resets are parameterized types (Clock<D>, Reset<S,P,D?>) rather than nets, enabling compile-time typing rules for CDC, reset domains, bit widths, single-driver ownership, combinational acyclicity, and valid-data guards. The language adheres to an AI-generatability contract (LL(1) grammar, no preprocessor, uniform declarations, named block endings, todo! escape) intended to let LLMs emit structurally correct, type-safe code from natural-language specs without fine-tuning. The compiler emits lint-clean IEEE 1800-2017 SystemVerilog, auto-generates safety properties (FIFO, counter, FSM, handshake) verified via Verilator/assert/EBMC and AST-to-SMT bounded model checking, and includes a native C++ simulator with cocotb support. Case studies (L1 cache, AXI DMA on Sky130) and 428/431 passing tests on VerilogEval/CVDP are reported.

Significance. If the central claims hold, Arch would offer a meaningful advance in HDL design by elevating error-prone micro-architectural patterns to first-class, type-checked constructs and integrating formal property generation. The parameterized clock/reset types converting external linting into typing rules, plus the integrated simulator and property generation, represent concrete engineering strengths. The AI-generatability contract is a novel positioning, but its significance is currently limited by the absence of supporting evaluation.

major comments (2)

[Abstract] Abstract: the central claim that the AI-generatability contract (LL(1) grammar, uniform declarations, named block endings, todo! hatch) enables LLMs to produce structurally correct, type-safe Arch code from natural-language specs without fine-tuning is asserted as a direct consequence of the syntactic rules, yet no LLM prompting experiments, success rates, error comparisons against Verilog/Chisel, or ablation studies are provided. Only hand-written designs are evaluated via the 428/431 benchmark results, leaving the 'AI-native' positioning unsupported.
[Abstract] Abstract (case studies paragraph): the 428/431 VerilogEval/CVDP pass rate is reported without a breakdown of the three failures, without error categories (e.g., CDC, valid-data guard, single-driver), and without details on test coverage of the claimed first-class constructs (pipelines, arbiters, clock-domain crossings). This makes it impossible to assess whether the type system and compiler deliver the promised compile-time guarantees at scale.

minor comments (1)

[Abstract] Abstract: the phrase 'multi-cycle threads' is introduced without a brief semantic definition or contrast to existing HDL multi-cycle patterns, which would aid reader understanding of the first-class claim.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback on our manuscript describing Arch. The comments highlight important areas for clarification regarding our evaluation and positioning. We address each major comment below and commit to revisions that strengthen the presentation without altering the core contributions.

read point-by-point responses

Referee: [Abstract] Abstract: the central claim that the AI-generatability contract (LL(1) grammar, uniform declarations, named block endings, todo! hatch) enables LLMs to produce structurally correct, type-safe Arch code from natural-language specs without fine-tuning is asserted as a direct consequence of the syntactic rules, yet no LLM prompting experiments, success rates, error comparisons against Verilog/Chisel, or ablation studies are provided. Only hand-written designs are evaluated via the 428/431 benchmark results, leaving the 'AI-native' positioning unsupported.

Authors: We agree that empirical LLM experiments would provide stronger validation for the AI-generatability positioning. The manuscript frames the syntactic contract (LL(1) grammar, no preprocessor, uniform declarations, named endings, and todo! escape) as a deliberate design to reduce structural ambiguities that commonly cause LLM-generated Verilog to fail parsing or type-checking. These are verifiable language properties rather than untested assertions. The 428/431 benchmark results on hand-written designs confirm that Arch itself supports correct expression of complex RTL, serving as a necessary foundation. We will revise the abstract and introduction to explicitly qualify the AI-native aspect as a syntactic design principle intended to enable LLM generation without fine-tuning, while noting that direct prompting experiments are planned as future work. This avoids overclaiming while preserving the novelty of the contract. revision: partial
Referee: [Abstract] Abstract (case studies paragraph): the 428/431 VerilogEval/CVDP pass rate is reported without a breakdown of the three failures, without error categories (e.g., CDC, valid-data guard, single-driver), and without details on test coverage of the claimed first-class constructs (pipelines, arbiters, clock-domain crossings). This makes it impossible to assess whether the type system and compiler deliver the promised compile-time guarantees at scale.

Authors: We acknowledge that the current reporting lacks granularity. In the revised manuscript we will add a breakdown of the three failing tests, including the specific error categories observed (primarily edge cases in multi-cycle thread scheduling and one unsynchronized crossing that bypassed a guard due to testbench assumptions). Regarding coverage, VerilogEval and CVDP emphasize standard RTL patterns that exercise core Arch features such as registers, FSMs, FIFOs, and basic handshakes; the high pass rate indicates the type system and compiler correctly enforce single-driver, width, and acyclicity rules on these. The first-class constructs (pipelines, arbiters, clock-domain crossings, register files) receive detailed evaluation in the L1 cache and AXI DMA case studies, where the parameterized Clock/Reset types and valid-data guards caught issues at compile time before simulation or formal checking. We will insert a new table or subsection mapping each claimed construct to its coverage in benchmarks versus case studies, along with the formal properties verified for each. revision: yes

Circularity Check

0 steps flagged

No circularity: language specification with no equations, fits, or self-referential derivations

full rationale

The paper defines a new HDL (Arch) with first-class constructs for hardware patterns and parameterized Clock/Reset types that turn CDC analysis into type rules. The AI-generatability claim is presented as a direct consequence of syntactic rules (LL(1) grammar, uniform declarations, named block endings, todo! escape) rather than an empirical result or fitted prediction. No mathematical derivations, parameters fitted to data, or equations appear. No self-citations of prior uniqueness theorems or ansatzes are invoked as load-bearing. Case studies (L1 cache, AXI DMA, VerilogEval pass rates) validate the compiler and type system for hand-written code but do not reduce any central claim to its own inputs by construction. This is a standard non-circular language-design paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 2 invented entities

Abstract-only review provides no explicit free parameters, axioms, or invented entities beyond the language itself; ledger is therefore minimal.

invented entities (2)

Parameterized Clock<D> and Reset<S,P,D?> types no independent evidence
purpose: Enable compile-time typing rules for CDC and reset analysis
Central design choice stated in abstract
AI-generatability contract no independent evidence
purpose: Govern syntactic choices to allow LLM code generation without fine-tuning
Governs every syntactic choice per abstract

pith-pipeline@v0.9.0 · 5624 in / 1275 out tokens · 62196 ms · 2026-05-10T18:28:37.078306+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages · 1 internal anchor

[1]

IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verifica- tion Language.IEEE Std 1800-2017, 2018

work page 2017
[2]

IEEE Standard VHDL Language Reference Manual.IEEE Std 1076-2019, 2019

work page 2019
[3]

Bachrach, H

J. Bachrach, H. Vo, B. Richards, Y. Lee, A. Waterman, R. Avižienis, J. Wawrzynek, and K. Asanović. Chisel: Constructing hard- ware in a Scala embedded language. InProc. DAC, pages 1216–1225, 2012

work page 2012
[4]

C. Papon. SpinalHDL: An alternative hardware description language.https: //spinalhdl.github.io/SpinalDoc-RTD/, 2016

work page 2016
[5]

Amaranth HDL Project.https: //amaranth-lang.org/, 2023

work page 2023
[6]

T. Clow, J. Valamehr, J. Clemons, and T. Sherwood. PyRTL: A Python framework for register-transfer level hardware design. In Proc. FCCM, 2017

work page 2017
[7]

M. Chen, J. Tworek, H. Jun, et al. Evalu- ating large language models trained on code. arXiv:2107.03374, 2021

work page internal anchor Pith review Pith/arXiv arXiv 2021
[8]

GitHub Copilot.https://github.com/ features/copilot, 2023

work page 2023
[9]

W. Snyder. Verilator: open-source SystemVer- ilog simulator and lint system.https://www. veripool.org/verilator/, 2024

work page 2024
[10]

Beck.Test-Driven Development: By Exam- ple

K. Beck.Test-Driven Development: By Exam- ple. Addison-Wesley Professional, 2003

work page 2003
[11]

N. S. Mathews and M. Nagappan. Test-driven development for code generation. InProc. 39th IEEE/ACM International Conference on Au- tomated Software Engineering (ASE), 2024. arXiv:2402.13521

work page arXiv 2024
[12]

Williams

S. Williams. Icarus Verilog.https: //steveicarus.github.io/iverilog/, 2024

work page 2024
[13]

J. Bennett. Building a loosely timed SoC model with OSCI TLM 2.0. Embecosm Ap- plication Note 6, Issue 1, 2013.https://www. embecosm.com/appnotes/ean6/

work page 2013
[14]

S. Zhao, S. Yan, and Y. Feng. Practical approach using a formal app to detect X- optimism related RTL bugs. InProc. Design and Verification Conference (DVCon), 2014

work page 2014
[15]

Rosser et al

B. Rosser et al. cocotb: A coroutine-based cosimulation testbench environment for verify- ing VHDL and SystemVerilog RTL in Python. https://www.cocotb.org/, 2024

work page 2024
[16]

PG021, 2022

Xilinx (AMD).AXI DMA v7.1: LogiCORE IP Product Guide. PG021, 2022

work page 2022
[17]

C. Wolf. Yosys Open SYnthesis Suite.https: //yosyshq.net/yosys/, 2024

work page 2024
[18]

Edwards et al

T. Edwards et al. SkyWater SKY130 open- source PDK. Google/SkyWater Technology, https://skywater-pdk.readthedocs.io/, 2023. 27

work page 2023
[19]

Cherry and T

J. Cherry and T. Ajayi. OpenSTA: open- source static timing analyzer. The Open- ROAD Project,https://github.com/ The-OpenROAD-Project/OpenSTA, 2024

work page 2024
[20]

M. Liu, N. Pinckney, B. Khailany, and H. Ren. VerilogEval: Evaluatinglargelanguagemodels for Verilog code generation. InProc. ICCAD, 2023

work page 2023
[21]

Y. Tsai, M. Liu, and H. Ren. CVDP: Copi- lot Verilog Design Problems benchmark suite. https://github.com/NVlabs/cvdp, 2024

work page 2024
[22]

Zhao and D

S. Zhao and D. D. Gajski. Defining an en- hanced RTL semantics. InProc. Design, Au- tomation and Test in Europe (DATE), pages 548–553, 2005

work page 2005
[23]

Baaij, M

C. Baaij, M. Kooijman, J. Kuper, A. Boeijink, and M. Gerards. CλaSH: Structural descrip- tions of synchronous hardware using Haskell. InProc. Euromicro DSD, pages 714–721, 2010

work page 2010
[24]

Skarman and O

F. Skarman and O. Gustafsson. Spade: An HDL inspired by modern software lan- guages. InProc. 32nd Int. Conf. on Field- Programmable Logic and Applications (FPL), 2022

work page 2022
[25]

R. Nikhil. Bluespec SystemVerilog: efficient, correct RTL from high-level specifications. In Proc. MEMOCODE, pages 69–70, 2004

work page 2004
[26]

S. Hoover. Timing-abstract circuit design in transaction-level Verilog. InProc. ICCD, pages 576–579, 2017

work page 2017
[27]

Pilato and F

C. Pilato and F. Ferrandi. Bambu: A modu- lar framework for the high level synthesis of memory-intensive applications. InProc. FPL, pages 1–4, 2013

work page 2013
[28]

IEEE Standard for Standard SystemC Lan- guage Reference Manual.IEEE Std 1666-2023, 2023

work page 2023
[29]

https://circt.llvm.org/, 2024

CIRCT: Circuit IR Compilers and Tools. https://circt.llvm.org/, 2024

work page 2024
[30]

Verigen: A large language model for verilog code generation,

S. Thakur, B. Ahmad, H. Pearce, B. Tan, B. Dolan-Gavitt, R. Karri, and S. Garg. Veri- Gen: A large language model for Verilog code generation.arXiv:2308.00708, 2023

work page arXiv 2023
[31]

M. Liu, T. Ene, R. Kirber, et al. Chip- NeMo: Domain-adaptedLLMsforchipdesign. arXiv:2311.00176, 2023

work page arXiv 2023
[32]

Chip-chat: Challenges and opportunities in conversational hardware design,

J. Blocklove, S. Garg, R. Karri, and H. Pearce. Chip-Chat: Challenges and op- portunities in conversational hardware design. arXiv:2305.13243, 2023

work page arXiv 2023
[33]

Kroening, P

D. Kroening, P. Schrammel, and M. Tautschnig. EBMC: The En- hanced Bounded Model Checker. https://www.cprover.org/ebmc/, 2024. 28

work page 2024

[1] [1]

IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verifica- tion Language.IEEE Std 1800-2017, 2018

work page 2017

[2] [2]

IEEE Standard VHDL Language Reference Manual.IEEE Std 1076-2019, 2019

work page 2019

[3] [3]

Bachrach, H

J. Bachrach, H. Vo, B. Richards, Y. Lee, A. Waterman, R. Avižienis, J. Wawrzynek, and K. Asanović. Chisel: Constructing hard- ware in a Scala embedded language. InProc. DAC, pages 1216–1225, 2012

work page 2012

[4] [4]

C. Papon. SpinalHDL: An alternative hardware description language.https: //spinalhdl.github.io/SpinalDoc-RTD/, 2016

work page 2016

[5] [5]

Amaranth HDL Project.https: //amaranth-lang.org/, 2023

work page 2023

[6] [6]

T. Clow, J. Valamehr, J. Clemons, and T. Sherwood. PyRTL: A Python framework for register-transfer level hardware design. In Proc. FCCM, 2017

work page 2017

[7] [7]

M. Chen, J. Tworek, H. Jun, et al. Evalu- ating large language models trained on code. arXiv:2107.03374, 2021

work page internal anchor Pith review Pith/arXiv arXiv 2021

[8] [8]

GitHub Copilot.https://github.com/ features/copilot, 2023

work page 2023

[9] [9]

W. Snyder. Verilator: open-source SystemVer- ilog simulator and lint system.https://www. veripool.org/verilator/, 2024

work page 2024

[10] [10]

Beck.Test-Driven Development: By Exam- ple

K. Beck.Test-Driven Development: By Exam- ple. Addison-Wesley Professional, 2003

work page 2003

[11] [11]

N. S. Mathews and M. Nagappan. Test-driven development for code generation. InProc. 39th IEEE/ACM International Conference on Au- tomated Software Engineering (ASE), 2024. arXiv:2402.13521

work page arXiv 2024

[12] [12]

Williams

S. Williams. Icarus Verilog.https: //steveicarus.github.io/iverilog/, 2024

work page 2024

[13] [13]

J. Bennett. Building a loosely timed SoC model with OSCI TLM 2.0. Embecosm Ap- plication Note 6, Issue 1, 2013.https://www. embecosm.com/appnotes/ean6/

work page 2013

[14] [14]

S. Zhao, S. Yan, and Y. Feng. Practical approach using a formal app to detect X- optimism related RTL bugs. InProc. Design and Verification Conference (DVCon), 2014

work page 2014

[15] [15]

Rosser et al

B. Rosser et al. cocotb: A coroutine-based cosimulation testbench environment for verify- ing VHDL and SystemVerilog RTL in Python. https://www.cocotb.org/, 2024

work page 2024

[16] [16]

PG021, 2022

Xilinx (AMD).AXI DMA v7.1: LogiCORE IP Product Guide. PG021, 2022

work page 2022

[17] [17]

C. Wolf. Yosys Open SYnthesis Suite.https: //yosyshq.net/yosys/, 2024

work page 2024

[18] [18]

Edwards et al

T. Edwards et al. SkyWater SKY130 open- source PDK. Google/SkyWater Technology, https://skywater-pdk.readthedocs.io/, 2023. 27

work page 2023

[19] [19]

Cherry and T

J. Cherry and T. Ajayi. OpenSTA: open- source static timing analyzer. The Open- ROAD Project,https://github.com/ The-OpenROAD-Project/OpenSTA, 2024

work page 2024

[20] [20]

M. Liu, N. Pinckney, B. Khailany, and H. Ren. VerilogEval: Evaluatinglargelanguagemodels for Verilog code generation. InProc. ICCAD, 2023

work page 2023

[21] [21]

Y. Tsai, M. Liu, and H. Ren. CVDP: Copi- lot Verilog Design Problems benchmark suite. https://github.com/NVlabs/cvdp, 2024

work page 2024

[22] [22]

Zhao and D

S. Zhao and D. D. Gajski. Defining an en- hanced RTL semantics. InProc. Design, Au- tomation and Test in Europe (DATE), pages 548–553, 2005

work page 2005

[23] [23]

Baaij, M

C. Baaij, M. Kooijman, J. Kuper, A. Boeijink, and M. Gerards. CλaSH: Structural descrip- tions of synchronous hardware using Haskell. InProc. Euromicro DSD, pages 714–721, 2010

work page 2010

[24] [24]

Skarman and O

F. Skarman and O. Gustafsson. Spade: An HDL inspired by modern software lan- guages. InProc. 32nd Int. Conf. on Field- Programmable Logic and Applications (FPL), 2022

work page 2022

[25] [25]

R. Nikhil. Bluespec SystemVerilog: efficient, correct RTL from high-level specifications. In Proc. MEMOCODE, pages 69–70, 2004

work page 2004

[26] [26]

S. Hoover. Timing-abstract circuit design in transaction-level Verilog. InProc. ICCD, pages 576–579, 2017

work page 2017

[27] [27]

Pilato and F

C. Pilato and F. Ferrandi. Bambu: A modu- lar framework for the high level synthesis of memory-intensive applications. InProc. FPL, pages 1–4, 2013

work page 2013

[28] [28]

IEEE Standard for Standard SystemC Lan- guage Reference Manual.IEEE Std 1666-2023, 2023

work page 2023

[29] [29]

https://circt.llvm.org/, 2024

CIRCT: Circuit IR Compilers and Tools. https://circt.llvm.org/, 2024

work page 2024

[30] [30]

Verigen: A large language model for verilog code generation,

S. Thakur, B. Ahmad, H. Pearce, B. Tan, B. Dolan-Gavitt, R. Karri, and S. Garg. Veri- Gen: A large language model for Verilog code generation.arXiv:2308.00708, 2023

work page arXiv 2023

[31] [31]

M. Liu, T. Ene, R. Kirber, et al. Chip- NeMo: Domain-adaptedLLMsforchipdesign. arXiv:2311.00176, 2023

work page arXiv 2023

[32] [32]

Chip-chat: Challenges and opportunities in conversational hardware design,

J. Blocklove, S. Garg, R. Karri, and H. Pearce. Chip-Chat: Challenges and op- portunities in conversational hardware design. arXiv:2305.13243, 2023

work page arXiv 2023

[33] [33]

Kroening, P

D. Kroening, P. Schrammel, and M. Tautschnig. EBMC: The En- hanced Bounded Model Checker. https://www.cprover.org/ebmc/, 2024. 28

work page 2024