{"id":"4fcc7c70-a366-4dd6-975e-e754cf6cdbed","arxiv_id":"2608.12684","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A contract-first, proof-guided multi-agent workflow can evolve validated RTL to a new version, demonstrated on a TPU datapath block adding TF32 support.","lead":"This paper proposes a workflow that updates a trusted, already-working hardware design (RTL) to a new version by first writing a precise, machine-checkable contract for the new behavior, then having AI agents plan, patch, and formally verify the changes. A generalist might read it because it targets a real engineering practice: most hardware changes are careful revisions of working designs, not from-scratch generation.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Verification success is reported via hw-cbmc, but no unwind bound or completeness argument is given; the forall-equivalence in Eq. (3) is therefore not established.","rationale":"The paper's contribution is a workflow, and the evidence for its central claim is the successful verification of the evolved RTL. That evidence is only as strong as the verification signal. Because the paper uses a bounded model checker without reporting bounds, the signal is ambiguous. This is not a disagreement with the hardware-verification consensus; it is an internal gap between the stated objective (forall-equivalence) and the reported method (BMC without completeness). The missing bound is directly checkable from the artifact, so the concern is actionable. Secondary issues such as model selection after seeing results and single runs affect generalizability but do not threaten the logical link between the workflow and the observed convergence as directly as the verification bound does. The paper is otherwise honest about its scope (functional, not PPA, evolution) and provides an artifact, which is why the appropriate verdict remains CONDITIONAL rather than REJECT; however, the bound must be disclosed and justified before the equivalence claim can be accepted.","tokens_in":15842,"tokens_out":4818,"duration_ms":50084,"concrete_test":"From the artifact's hw-cbmc invocation scripts, extract the exact --unwind/--depth bound k used for the final dot_core verification. Independently re-run the same verification with k+1 and, if the state space permits, use k-induction or compute the sequential diameter to determine a completeness threshold. If a counterexample appears at any depth > k, then the reported PASS does not establish Eq. (3) and the headline result should be weakened to bounded convergence. If no counterexample appears beyond k and a completeness argument is supplied, the objection is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central correctness objective is Eq. (3): R_{N+1} |= C_{N+1}, defined by the forall-equivalence in Eq. (2) over all legal transactions. The paper establishes this with hw-cbmc (Sections 4.4, 5.1), a bounded model checker, yet nowhere reports the unwind depth, loop bound, or a completeness threshold for the checks. Consequently, a PASS only shows absence of counterexamples up to some unstated depth k. For a sequential datapath with pipeline state, interactions beyond k are unchecked; an RTL that diverges from the contract at transaction depth k+1 would still pass. The claim of 'functional convergence' in the abstract and Section 6 is thus stronger than the evidence. A related concern is that T_v itself is defined by the harness's assume clauses; the paper states these are reviewed for soundness (Section 4.2) but does not prove that they exactly characterize legal transactions, so an over-restrictive assume would make Eq. (2) vacuous for missing legal inputs. Both issues share the same remedy: report and justify the verification bound.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":16007,"tokens_out":6006,"duration_ms":57221,"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":[{"comment":"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.","section":"§4.4, §5.1, Eqs. (2)–(3)"},{"comment":"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.","section":"§4.2, Eq. (2)"},{"comment":"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.","section":"§5.1, §5.2, §5.4"}],"minor_comments":[{"comment":"The abstract contains a typo: \"We presentspec-driven hardware evolution\" should read \"We present spec-driven hardware evolution\".","section":"Abstract"},{"comment":"The affiliation city \"Nanjign, China\" is misspelled (twice); it should be \"Nanjing, China\".","section":"Affiliations"},{"comment":"In the workflow diagram, the label \"Cases Test\" should read \"Test Cases\".","section":"Fig. 2"},{"comment":"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.","section":"Eq. (4)"},{"comment":"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.","section":"Fig. 4(e)–(f)"},{"comment":"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.","section":"Algorithm 1 and §4.3"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a plausible case study, but the evidentiary base is thin: one task, one run per condition, bounded verification depth not reported, and the front-end Specify stage excluded from the quantitative evaluation. If the authors cannot add experiments, they should substantially soften the convergence claims. The artifact and the external contract-based evaluation criterion are strengths."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my read.\n\nThe genuinely new thing is the problem formulation: treating a next-version RTL update as refinement under a reviewed executable contract, instead of prompt-to-RTL generation. The four-stage Specify-Plan-Implement-Validate split is sensible, and the mutation-based semantic probing for correspondence mapping is a concrete, useful idea. Showing this on a real TPU datapath block (dot_core, TF32 update) with several models and cost data is a real feasibility demonstration, not a toy. Credit also for the ablations: removing subagents, probing, hierarchy-aware repair, or the structured plan all measurably hurt, which gives some confidence the components matter.\n\nThe soft spots are exactly where the reader's report put them. First, the verification is hw-cbmc, a bounded model checker, and the paper never reports unwind depths or any completeness threshold. Eq. (3) claims forall-equivalence over all legal transactions; a PASS only shows no counterexample up to some unstated bound. The abstract's 'functional convergence' is stronger than the evidence. This is fixable by reporting bounds and adding an unbounded check or at least stating the checked depth.\n\nSecond, the evidence is one task, one run per condition. The default model for ablations (GPT-5.4) was selected after seeing the main results, which weakens subsequent comparisons. Contract construction is excluded from evaluation, and the human-review quality of the harness is not measured. None of these are fatal, but they should be stated more carefully. The workflow-vs-LangGraph comparison is muddled: one run each, and the proposed workflow uses 8x more tokens, which they attribute to flexibility. Maybe true, but with one run it is hard to say.\n\nOn the citation side, the related work seems fair, and the self-citations to FormalRTL and CktEvo are legitimate.\n\nOverall: a useful, well-structured paper with a real new formulation and a plausible single-case demonstration. It is not a breakthrough, but it deserves a serious referee. I would send it to review with a request for verification bounds, repeated runs, and a more careful statement of what the BMC PASS means.","headline":"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.","tokens_in":16598,"tokens_out":3117,"would_cite":true,"duration_ms":31822,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["spec-driven hardware evolution","executable contract","RTL version evolution","mutation-based semantic probing","proof-guided RTL update","hw-cbmc","TPU datapath","legacy-aware repair"],"falsifier":"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.","tokens_in":15582,"feed_emoji":"⚙️","tokens_out":6060,"duration_ms":54596,"temperature":0.7,"pith_summary":"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.","feed_headline":"Contract-checked loop evolves legacy RTL to next versions","feed_subtitle":"A TPU datapath block reaches functional convergence in as few as two repair iterations, preserving validated logic.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Establishes behavioral consistency checking of C and Verilog programs via bounded model checking, the methodological basis for the contract harness and hw-cbmc checking.","marker":"[7]"},{"why":"Provides the TPU datapath block (dot_core) used as the controlled legacy design in the evaluation.","marker":"[14]"},{"why":"Supplies hw-cbmc, the formal verification backend that checks R_{N+1} against the executable contract.","marker":"[25]"},{"why":"Defines TF32 data-format semantics, which constitute the version-N to version-N+1 feature change in the case study.","marker":"[33]"}],"fun_headline_variants":["Executable contracts steer legacy RTL to next versions","Proof-guided RTL update via contract refinement","Contract-centered loop evolves hardware datapath","RTL evolution with executable contracts and proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Executable contracts steer legacy RTL to next versions","Proof-guided RTL update via contract refinement","Contract-centered loop evolves hardware datapath","RTL evolution with executable contracts and proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000148,"raw_usage":{"total_tokens":1223,"prompt_tokens":1011,"completion_tokens":212,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":627,"completion_tokens_details":{"reasoning_tokens":155}},"tokens_in":627,"tokens_out":212,"duration_ms":2745,"temperature":1.0,"reasoning_tokens":155,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:39:18.239823+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes behavioral consistency checking of C and Verilog programs via bounded model checking, the methodological basis for the contract harness and hw-cbmc checking."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies hw-cbmc, the formal verification backend that checks R_{N+1} against the executable contract."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines TF32 data-format semantics, which constitute the version-N to version-N+1 feature change in the case study."}],"review_version":1}