Pith. sign in

REVIEW 3 major objections 6 minor 47 references

Spec-Driven Hardware Evolution via Executable Contract Refinement and Proof-Guided RTL Update

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

Pith's one-line read A contract-centered workflow can evolve validated legacy RTL to satisfy a next-version specification through proof-guided, localized repair rather than regeneration from scratch.

desk verdict New workflow formulation for RTL version evolution, with a plausible single-case feasibility demo, undermined mainly by unreported BMC bounds and one-run comparisons; worth serious review. read the letter →

arxiv 2608.12684 v1 pith:TZMOVYZR submitted 2026-08-13 cs.AR

classification cs.AR
keywords spec-drivenhardwareevolutionexecutablecontractRTLversionmutation-basedsemanticprobingproof-guidedupdatehw-cbmcTPUdatapathlegacy-awarerepair
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 hardware version updates should be treated as contract-driven evolution, not prompt-to-RTL generation: the next version's intended behavior is captured as a reviewed executable contract, and the legacy RTL is then updated and formally checked against that contract until it converges. The central claim is that this backend workflow can drive validated legacy RTL to functional convergence for the next version, demonstrated on a TPU datapath block undergoing a data-format change. Why it matters: hardware maintenance mostly means revising a trusted design, and if the contract is the semantic target, a large language model can make localized, proof-guided edits instead of regenerating RTL. The paper reports that top models converge within a few repair iterations, with ablation studies attributing reliability to task-isolated subagents, mutation-based semantic probing, hierarchy-aware bottom-up repair, and structured planning.

What carries the argument

The load-bearing object is the executable contract C_v = (M_v, Phi_v): M_v is a software reference, and Phi_v is the harness that fixes interface, observation, and timing semantics through assume clauses, next_timeframe(), and assert clauses, making the contract consumable by the hw-cbmc bounded-model-checking backend. Around it, the Plan stage's mutation-based semantic probing injects controlled faults into the legacy RTL and reads the verification feedback to build contract_rtl_map, a verified mapping from contract outcomes to RTL regions that localizes the change; the Implement/Validate loop then patches the legacy RTL under that guidance and iterates on counterexamples until Eq. (3) holds.

What would settle it

Place the entire semantic delta of a version change inside a region that mutation-based probing marks as a blind spot; if the workflow then reports convergence under hw-cbmc but the evolved RTL fails on a legal transaction that exercises that region at a depth beyond the checked bound, the bounded verification is too shallow to establish the claimed equivalence.

Watch

Extended reading notes

Core claim

The paper's discovery is the formulation itself plus the evidence that it works: defining version N+1 by an executable contract C_{N+1} = (M_{N+1}, Phi_{N+1}) — a behavior-level C/C++ reference plus a harness encoding assume clauses, next_timeframe() alignment, and assert relations — and then evolving legacy RTL R_N through a Plan-Implement-Validate loop that uses hw-cbmc counterexamples as repair feedback can achieve R_{N+1} |= C_{N+1}. On the dot_core TPU datapath with TF32 support added, the workflow converges in as few as two iterations for the best-performing model and within four for other top models, and ablations show that removing any of the four supporting mechanisms degrades or breaks convergence. The paper frames this as functional convergence, explicitly leaving PPA optimization to downstream flows.

Load-bearing premise

The load-bearing premise is that the human-reviewed executable contract for version N+1 — its reference model, harness assumptions, timing alignment, and assertions — is a complete and correct statement of the intended behavior, so that a passing formal check truly means the evolved RTL matches the intent for all legal transactions.

Editorial extensions

If this is right

  • Once a next-version contract is approved, the remaining Specify-Plan-Implement-Validate stages can run without human intervention, turning version evolution into an automated, formally checkable loop.
  • Validated legacy logic is preserved wherever possible: edits are localized to regions implicated by the semantic delta and the contract-to-RTL mapping, so trusted behavior is not regenerated from scratch.
  • Formal verification feedback is used not merely as a pass/fail filter but as the organizing signal that localizes faults, guides repair, and decides when the contract itself must be revised.
  • Mutation-based probing exposes blind spots in the legacy design — signals insensitive to injected faults — which the planner treats conservatively as low-confidence regions for extra scrutiny during validation.
  • The evolved RTL is intended as a functionally converged starting point for downstream PPA-oriented refinement, separating functional evolution from physical design optimization.

Reading between the lines

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

  • If this scales beyond the single datapath case, the human role in hardware maintenance shifts from writing and debugging RTL to reviewing contracts, which could lower the entry barrier for routine version bumps.
  • Blind spots are a natural audit mechanism: a region that cannot be proven sensitive to any mutation should arguably block sign-off or require additional constraints, a policy the paper observes but does not enforce.
  • The same contract-centered loop should transfer to interface and timing changes, not just data-format changes, because the contract semantics (assume/next_timeframe/assert) are expressed independently of the datapath arithmetic.
  • A testable extension: instrument the loop to record how often validation failure escalates to contract revision rather than RTL repair; the paper's convergence numbers alone do not reveal how frequently the contract itself had to be weakened.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. The paper proposes a contract-centered workflow for evolving validated legacy RTL to a next version. The workflow has four stages: Specify refines a feature request into a human-reviewed executable contract (a C/C++ reference model plus a harness encoding assume, next_timeframe(), and assert semantics); Plan derives the cross-version semantic delta and localizes affected RTL regions using mutation-based semantic probing; Implement performs localized legacy-aware patching; Validate checks the candidate with hw-cbmc against the contract and feeds counterexamples into iterative repair. The formal objective is Eq. (3), R_{N+1} |= C_{N+1}, under the transactional equivalence in Eq. (2). The evaluation is a single version-evolution task on a TPU datapath block (dot_core) adding TF32 support, run across seven LLMs, plus ablations of subagent isolation, semantic probing, hierarchy-aware repair, and structured planning. The paper reports that three models converge, that GPT-5.4 is the most efficient successful model, and that the full workflow outperforms the ablated variants on iteration count and cost.

Significance. If the results hold, the paper makes a useful contribution by reframing RTL version iteration as contract-driven evolution rather than prompt-to-RTL generation. The evaluation criterion is externally anchored: RTL is checked with hw-cbmc against a human-reviewed executable contract, so the central success metric is not circularly defined by the paper's own outputs. The ablation study and the anonymous artifact support reproducibility, and the distinction between contract construction and automated backend evolution is clearly drawn. The main limitations are evidentiary: one task, one run per condition, a Specify stage excluded from the quantitative evaluation, and an unstated bounded-verification depth. As a feasibility case study the paper is suggestive, but it does not yet establish a general methodology for contract-driven hardware evolution.

major comments (3)
  1. [§4.4, §5.1, Eqs. (2)–(3)] The paper reports hw-cbmc PASS as establishing R_{N+1} |= C_{N+1}, but hw-cbmc is a bounded model checker and no unwind depth, loop bound, or completeness threshold is reported anywhere in Sections 4.4 or 5.1. Since Eq. (2) quantifies over all legal transactions and the RTL is a sequential pipelined datapath with next_timeframe() alignment, a PASS merely shows absence of counterexamples up to some unstated bound; an implementation that diverges at a deeper transaction or after more pipeline stages would still pass. The abstract and Section 6 therefore claim "functional convergence" more strongly than the evidence supports. Please report the exact verification bound used for every reported PASS, justify that the bound covers all legal transactions (or use an unbounded or inductive proof), and qualify the convergence claims accordingly.
  2. [§4.2, Eq. (2)] The universal quantification in Eq. (2) is over T_v, the set of legal transactions induced by the contract's assume clauses, but the paper does not establish that the reviewed harness exactly characterizes the intended legal input domain. Section 4.2 states that assume clauses are "examined" and the contract is human-reviewed, but no coverage criteria, counterexample analysis, or independent check is reported. If an assume clause is too restrictive, Eq. (2) becomes vacuous for the excluded legal inputs and a verification PASS is misleading; if it is too permissive, the checked equivalence is stronger than intended and may produce spurious failures. This is load-bearing because the contract is the external ground truth for the whole evaluation. Please provide evidence that the harness's assume, next_timeframe, and assert clauses characterize the intended transactional semantics, or explicitly redefine Eq. (2) as equivalence relative to the harness-defined T_v and adjust the claims accordingly.
  3. [§5.1, §5.2, §5.4] The quantitative evaluation is a single version-evolution task (dot_core) with one run per model and per ablation condition. All reported comparisons, such as the 2-versus-4-versus-3 iteration differences in Fig. 4(a) and the $15.65-versus-$55.75 cost differences, are single observations with no variance estimate, so the ranking of models and the ablation effects cannot be distinguished from sampling noise. In addition, the Specify stage is excluded from the evaluation by design, even though executable-contract refinement is one of the paper's stated contributions. As a feasibility case study the evidence is suggestive, but it does not yet support the general statement that the workflow "can effectively drive" legacy RTL to convergence across settings. Please add at least one additional evolution task or multiple runs per condition, and report the validation performed on the contract-construction stage.
minor comments (6)
  1. [Abstract] The abstract contains a typo: "We presentspec-driven hardware evolution" should read "We present spec-driven hardware evolution".
  2. [Affiliations] The affiliation city "Nanjign, China" is misspelled (twice); it should be "Nanjing, China".
  3. [Fig. 2] In the workflow diagram, the label "Cases Test" should read "Test Cases".
  4. [Eq. (4)] The semantic delta notation Diff(C_N, C_N+1) is introduced without a formal definition; please specify whether it is a syntactic diff on the reference and harness or a behavioral relation over transactions.
  5. [Fig. 4(e)–(f)] The legend "Converged Failed (reached max iter)" is ambiguous; please clarify that "Failed" refers to models whose runs exhausted the 20-iteration budget without top-level verification.
  6. [Algorithm 1 and §4.3] In Algorithm 1, a mutant that passes hw-cbmc is immediately classified as a blind spot, but a pass could also mean the injected fault is not actually observable because the signal is unused or the mutation is masked; please clarify how this confound is handled.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the backend's success criterion is an externally posed, human-reviewed contract checked by an independent verifier (hw-cbmc), not an output-redefined quantity.

full rationale

The paper's central objective, Eq. (3), is contract satisfaction R_{N+1} |= C_{N+1}, defined in Eq. (2) as transactional equivalence between the RTL and the reviewed executable contract. The contract C_{N+1} is constructed from the legacy contract and the feature request in the Specify stage and is fixed and human-reviewed before backend automation begins, as stated in Sections 4.2 and 5.1. The backend Plan/Implement/Validate loop uses hw-cbmc, an independent bounded model checker cited as [25], as the verification oracle; the mutation-based semantic probing in Section 4.3 also uses hw-cbmc, but against the legacy contract C_N to build planning correspondences, not against C_{N+1} to define success. No equation is shown to reduce to another by construction, and no fitted parameter or calibration step is renamed as a prediction: the reported metrics (iterations, tokens, cost, time, PPA) are measured outcomes of running the workflow, not outputs forced by the inputs. The only self-citations are FormalRTL [16] and CktEvo [29], and they appear in related-work positioning and as downstream PPA suggestions rather than as load-bearing evidence for the convergence claim; neither is invoked as a uniqueness theorem or as the source of the verification result. The absence of a reported hw-cbmc unwind bound or completeness threshold is a legitimate verification-strength limitation because Eq. (2) is a forall quantification, but that is a soundness concern about whether a PASS establishes the claimed equivalence, not circularity in the derivation chain. Overall, the paper is self-contained against an external, human-reviewed target and an independent verifier, so the circularity score is 0.

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

The central feasibility claim rests on (1) the trustworthiness of the legacy RTL and contract, (2) the correctness and completeness of the human-reviewed next-version contract, (3) the soundness of hw-cbmc as the equivalence oracle, and (4) the validity of the mutation-probing heuristic. The paper provides an empirical demonstration but does not independently justify these assumptions; they are all domain assumptions or paper-specific heuristics. No free parameters are fitted to data in a statistical sense, but several configuration choices (iteration budget, mutant set, model selection) strongly influence the reported outcomes.

free parameters (3)
  • max repair iterations (max_repair) = 20
    Convergence is defined as verification success within this budget. A larger budget could change which models are counted as converged, affecting the cross-model and ablation conclusions. No sensitivity analysis is reported.
  • mutation fault set and probing configuration = Unspecified; includes shift-direction errors, sign inversions, branch negations
    The contract_rtl_map quality and localization depend on the mutant types and counts, which are not reported precisely, so the Plan stage's contribution is hard to reproduce or assess.
  • default model for ablations = GPT-5.4
    GPT-5.4 was selected after observing its convergence results; all orchestration and ablation comparisons use only this model, so component contributions are demonstrated on one favorable backend.
assumptions (4)
  • domain assumption R_N is a validated implementation of C_N (R_N |= C_N).
    The workflow treats legacy RTL as trusted without re-verifying it. If latent bugs exist, the semantic delta and probing start from a false baseline. Invoked in Sections 1 and 3 as input artifacts.
  • domain assumption The human-reviewed contract C_{N+1} (C reference plus harness) completely and correctly captures next-version intent.
    Specify is excluded from quantitative evaluation, and the contract is treated as ground truth. An incomplete or wrong contract would make verification success irrelevant to true intent. Invoked in Sections 4.2 and 5.1.
  • domain assumption hw-cbmc with the supplied harness and bounds is sound and sufficiently complete for Eq. (2) transactional equivalence.
    All validation and probing results rest on hw-cbmc. BMC has coverage limits, yet the paper states Eq. (2) as a forall statement and calls the loop 'proof-guided' without reporting unwinding bounds. Invoked in Sections 4.1, 4.4, and 5.1.
  • ad hoc to paper Mutation-based semantic probing's sensitivity signal identifies semantically relevant RTL regions.
    The Plan stage treats fault-responsive signals as verified correspondences and insensitive ones as blind spots. Insensitivity could also arise from inactive mutants, so the heuristic may misclassify regions. This is a paper-specific premise, not an established technique. Invoked in Section 4.3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Spec-Driven Hardware Evolution via Executable Contract Refinement and Proof-Guided RTL Update." pith.science (2026). https://pith.science/paper/TZMOVYZR

@misc{pith2026260812684,
  author       = {Pith},
  title        = {Pith review of: Spec-Driven Hardware Evolution via Executable Contract Refinement and Proof-Guided RTL Update},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TZMOVYZR}},
  note         = {Machine review of arXiv:2608.12684}
}
read the original abstract

Hardware development is inherently evolutionary: major revisions typically begin by changing intended behavior and then updating a previously validated implementation, rather than regenerating RTL from scratch. Yet most recent LLM-based hardware research still frames the task primarily as prompt-to-RTL generation, offering limited support for semantic version evolution of trusted legacy designs. We present spec-driven hardware evolution, a contract-centered formulation for RTL version iteration. Instead of treating a new feature request as a direct prompt for RTL generation, we refine it into a reviewed executable contract for the next version. This contract specifies what must hold at the externally visible transactional level through a behavior-level reference together with explicit observation and checking semantics, while leaving how the change is realized in RTL to the evolution process. Based on this formulation, we organize hardware evolution into four stages: Specify, Plan, Implement, and Validate. After contract approval, the remaining stages proceed automatically: Plan derives cross-version semantic deltas and localizes affected RTL regions, aided by mutation-based semantic probing; Implement and Validate then perform legacy-aware RTL update under proof-guided checking and iterative repair. We evaluate the framework on a controlled version-evolution case study of a representative TPU datapath block under data-format changes. The results support the feasibility of contract-driven hardware evolution and demonstrate that the proposed backend workflow can effectively drive validated legacy RTL toward next-version functional convergence under a reviewed executable contract. An anonymous artifact for reproducibility is available at https://anonymous.4open.science/r/SDHE-3A6C.

Figures

Figures reproduced from arXiv: 2608.12684 by the authors.

Figure 1
Figure 1. Spec-driven hardware evolution workflow. Human [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Overall workflow of the proposed spec-driven hardware evolution framework. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Mutation-based semantic probing procedure and [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Comparison of repair iterations, token usage, mon [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Ablation results on dot_core evolution. (1) w/o task-isolated subagents, which removes fresh sub-agent iso￾lation while keeping the same overall workflow. (2) w/o mutation-based semantic probing, which disables mutation￾guided semantic localization in the planning stag…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 20 canonical work pages

  1. [1]

    Armin Abdollahi, Saeid Shokoufa, Negin Ashrafi, Mehdi Kamal, and Massoud Pedram. 2026. HDLFORGE: A Two-Stage Multi-Agent Framework for Effi- cient Verilog Code Generation with Adaptive Model Escalation.arXiv preprint arXiv:2603.04646(2026)

  2. [2]

    Ahmed Allam, Youssef Mansour, and Mohamed Shalan. 2025. ASIC-Agent: An Autonomous Multi-Agent System for ASIC Design with Benchmark Evaluation. In2025 IEEE International Conference on LLM-Aided Design (ICLAD). IEEE, 23–29

  3. [3]

    Nathan Binkert, Bradford Beckmann, Gabriel Black, Steven K Reinhardt, Ali Saidi, Arkaprava Basu, Joel Hestness, Derek R Hower, Tushar Krishna, Somayeh Sardashti, et al. 2011. The gem5 simulator.ACM SIGARCH computer architecture news39, 2 (2011), 1–7

  4. [4]

    Jason Blocklove, Shailja Thakur, Benjamin Tan, Hammond Pearce, Siddharth Garg, and Ramesh Karri. 2025. Automatically improving llm-based verilog generation using eda tool feedback.ACM Transactions on Design Automation of Electronic Systems(2025)

  5. [5]

    Manuel Blum and Hal Wasserman. 2002. Reflections on the Pentium division bug.IEEE Trans. Comput.45, 4 (2002), 385–393

  6. [6]

    Islem Bouzenia, Premkumar Devanbu, and Michael Pradel. 2025. Repairagent: An autonomous, llm-based agent for program repair. In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2188–2200

  7. [7]

    Edmund Clarke, Daniel Kroening, and Karen Yorav. 2003. Behavioral consistency of C and Verilog programs using bounded model checking. InProceedings of the 40th annual Design Automation Conference. 368–371

  8. [8]

    Fan Cui, Chenyang Yin, Kexing Zhou, Youwei Xiao, Guangyu Sun, Qiang Xu, Qipeng Guo, Yun Liang, Xingcheng Zhang, Demin Song, et al. 2024. Origen: En- hancing rtl code generation with code-to-code augmentation and self-reflection. InProceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design. 1–9

Show all 47 references
  1. [9]

    Mingzhe Gao, Jieru Zhao, Zhe Lin, Wenchao Ding, Xiaofeng Hou, Yu Feng, Chao Li, and Minyi Guo. 2024. Autovcoder: A systematic framework for automated verilog code generation using llms. In2024 IEEE 42nd International Conference on Computer Design (ICCD). IEEE, 162–169

  2. [10]

    Ping Guo, Yiting Wang, Wanghao Ye, Yexiao He, Ziyao Wang, Xiaopeng Dai, Ang Li, and Qingfu Zhang. 2025. EvoVerilog: Large Langugage Model Assisted Evolution of Verilog Code.arXiv preprint arXiv:2508.13156(2025)

  3. [11]

    Chia-Tung Ho, Haoxing Ren, and Brucek Khailany. 2025. Verilogcoder: Au- tonomous verilog coding agents with graph-based planning and abstract syntax tree (ast)-based waveform tracing tool. InProceedings of the AAAI Conference on Artificial Intelligence, Vol. 39. 300–307

  4. [12]

    Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2023. Swe-bench: Can language models resolve real-world github issues?arXiv preprint arXiv:2310.06770(2023)

  5. [13]

    Pengwei Jin, Di Huang, Chongxiao Li, Shuyao Cheng, Yang Zhao, Xinyao Zheng, Jiaguo Zhu, Shuyi Xing, Bohan Dou, Rui Zhang, et al. 2025. Realbench: Bench- marking verilog generation models with real-world ip designs.arXiv preprint arXiv:2507.16200(2025)

  6. [14]

    Norman P Jouppi, Cliff Young, Nishant Patil, David Patterson, Gaurav Agrawal, Raminder Bajwa, Sarah Bates, Suresh Bhatia, Nan Boden, Al Borchers, et al. 2017. In-datacenter performance analysis of a tensor processing unit. InProceedings of the 44th annual international symposi...

  7. [15]

    Sakari Lahti, Panu Sjövall, Jarno Vanne, and Timo D Hämäläinen. 2018. Are we there yet? A study on the state of high-level synthesis.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems38, 5 (2018), 898–911

  8. [16]

    Kezhi Li, Min Li, Xiangyu Wen, Shibo Zhao, Jieying Wu, Junhua Huang, and Qiang Xu. 2026. FormalRTL: Verified RTL Synthesis at Scale.arXiv preprint arXiv:2603.08738(2026)

  9. [17]

    Mengming Li, Wenji Fang, Qijun Zhang, and Zhiyao Xie. 2025. Specllm: Exploring generation and review of vlsi design specification with large language model. In 2025 International Symposium of Electronics Design Automation (ISEDA). IEEE, 749–755

  10. [18]

    Mingjie Liu, Nathaniel Pinckney, Brucek Khailany, and Haoxing Ren. 2023. Ver- ilogEval: Evaluating Large Language Models for Verilog Code Generation. In 2023 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

  11. [19]

    Qingyuan Liu, Mo Zou, Hengbin Zhang, Dong Du, Yubin Xia, and Haibo Chen

  12. [20]

    Shang Liu, Wenji Fang, Yao Lu, Jing Wang, Qijun Zhang, Hongce Zhang, and Zhiyao Xie. 2024. Rtlcoder: Fully open-source and efficient llm-assisted rtl code generation technique.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems(2024)

  13. [21]

    Yao Liu, Lu, Wenji Fang, Mengming Li, and Zhiyao Xie. 2024. Openllm-rtl: Open dataset and benchmark for llm-aided design rtl generation. InProceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design. 1–9

  14. [22]

    Yao Lu, Shang Liu, Qijun Zhang, and Zhiyao Xie. 2024. RTLLM: An Open-Source Benchmark for Design RTL Generation with Large Language Model. In2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC). IEEE, 722–727

  15. [23]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. Specgen: Automated generation of formal program specifications via large language models. In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 16–28

  16. [24]

    Ruiyang Ma, Daikang Kuang, Ziqian Liu, Jiaxi Zhang, Ping Fan, and Guojie Luo

  17. [25]

    Rajdeep Mukherjee, Mitra Purandare, Raphael Polig, and Daniel Kroening. 2017. Formal techniques for effective co-verification of hardware/software co-designs. InProceedings of the 54th Annual Design Automation Conference 2017. 1–6

  18. [26]

    Hongyang Pan, Cunqing Lan, Yiting Liu, Zhiang Wang, Li Shang, Xuan Zeng, Fan Yang, and Keren Zhu. 2024. Physically aware synthesis revisited: guiding technology mapping with primitive logic gate placement. InProceedings of the 43rd IEEE/ACM International Conference on Computer...

  19. [27]

    Zehua Pei, Hui-Ling Zhen, Mingxuan Yuan, Yu Huang, and Bei Yu. 2024. BetterV: controlled verilog generation with discriminative guidance. InProceedings of the 41st International Conference on Machine Learning. 40145–40153

  20. [28]

    Deepak Babu Piskala. 2026. Spec-Driven Development: From Code to Contract in the Age of AI Coding Assistants.arXiv preprint arXiv:2602.00180(2026)

  21. [29]

    Zhengyuan Shi, Jingxin Wang, Tairan Cheng, Changran Xu, Weikang Qian, and Qiang Xu. 2026. CktEvo: Repository-Level RTL Code Benchmark for Design Evolution.arXiv preprint arXiv:2603.08718(2026)

  22. [30]

    Kimia Tasnia, Alexander Garcia, Tasnuva Farheen, and Sazadur Rahman. 2025. Veriopt: Ppa-aware high-quality verilog generation via multi-role llms.arXiv preprint arXiv:2507.14776(2025)

  23. [31]

    Minh VT Thai, Tue Le, Dung Nguyen Manh, Huy Phan Nhat, and Nghi DQ Bui. 2025. SWE-EVO: Benchmarking Coding Agents in Long-Horizon Software Evolution Scenarios.arXiv preprint arXiv:2512.18470(2025)

  24. [32]

    Shailja Thakur, Baleegh Ahmad, Hammond Pearce, Benjamin Tan, Brendan Dolan- Gavitt, Ramesh Karri, and Siddharth Garg. 2024. Verigen: A large language model for verilog code generation.ACM Transactions on Design Automation of Electronic Systems29, 3 (2024), 1–31

  25. [33]

    Pedro Valero-Lara, Ian Jorquera, Frank Lui, and Jeffrey Vetter. 2023. Mixed- precision s/dgemm using the tf32 and tf64 frameworks on low-precision ai tensor cores. InProceedings of the SC’23 Workshops of the International Conference on High Performance Computing, Network, Stor...

  26. [34]

    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 Design (ICCAD). 992–998. doi:10.1109/ICCAD.2017.8203889

  27. [35]

    Yiting Wang, Guoheng Sun, Wanghao Ye, Gang Qu, and Ang Li. 2025. VeriRea- son: Reinforcement Learning with Testbench Feedback for Reasoning-Enhanced 9 Verilog Generation.arXiv preprint arXiv:2505.11849(2025)

  28. [36]

    Yangbo Wei, Zhen Huang, Huang Li, Wei W Xing, Ting-Jung Lin, and Lei He

  29. [37]

    Chunqiu Steven Xia and Lingming Zhang. 2024. Automated Program Repair via Conversation: Fixing 162 out of 337 Bugs for $0.42 Each using ChatGPT. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. 819–831

  30. [38]

    Zhiyuan Yan, Wenji Fang, Mengming Li, Min Li, Shang Liu, Zhiyao Xie, and Hongce Zhang. 2025. Assertllm: Generating hardware verification assertions from design specifications via multi-llms. InProceedings of the 30th Asia and South Pacific Design Automation Conference. 614–621

  31. [39]

    Vflow: Discovering optimal agentic workflows for verilog generation.arXiv preprint arXiv:2504.03723(2025)

  32. [40]

    John Yang, Akshara Prabhakar, Karthik Narasimhan, and Shunyu Yao. 2023. Intercode: Standardizing and benchmarking interactive coding with execution feedback.Advances in Neural Information Processing Systems36 (2023), 23826– 23854

  33. [41]

    Kechi Zhang, Jia Li, Ge Li, Xianjie Shi, and Zhi Jin. 2024. Codeagent: Enhancing code generation with tool-integrated agent systems for real-world repo-level coding challenges. InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1:...

  34. [42]

    John Yang, Carlos E Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press. 2024. Swe-agent: Agent-computer interfaces enable automated software engineering.Advances in Neural Information Processing Systems37 (2024), 50528–50652

  35. [43]

    Yujie Zhao, Hejia Zhang, Hanxian Huang, Zhongming Yu, and Jishen Zhao. 2025. Mage: A multi-agent engine for automated rtl code generation. In2025 62nd ACM/IEEE Design Automation Conference (DAC). IEEE, 1–7

  36. [44]

    Yaoyu Zhu, Di Huang, Hanqi Lyu, Xiaoyun Zhang, Chongxiao Li, Wenxuan Shi, Yutong Wu, Jianan Mu, Jinghua Wang, Yang Zhao, et al. 2025. CodeV-R1: Reasoning-Enhanced Verilog Generation.arXiv preprint arXiv:2505.24183(2025). 10

  37. [45]

    Yang Zhao, Di Huang, Chongxiao Li, Pengwei Jin, Muxin Song, Yinan Xu, Ziyuan Nan, Mingju Gao, Tianyun Ma, Lei Qi, et al . 2025. Codev: Empowering llms with hdl generation through multi-level summarization.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Sy...

  38. [2025]

    In2025 IEEE/ACM International Conference On Computer Aided Design (ICCAD)

    Wit-HW: Bug Localization in Hardware Design Code via Witness Test Case Generation. In2025 IEEE/ACM International Conference On Computer Aided Design (ICCAD). IEEE, 1–9

  39. [2026]

    In24th USENIX Conference on File and Storage Technologies (FAST 26)

    Sharpen the Spec, Cut the Code: A Case for Generative File System with {SYSSPEC}. In24th USENIX Conference on File and Storage Technologies (FAST 26). 291–311

Pith tools

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