{"id":"5f34fa26-504c-4027-b9cd-49e91a6e6a18","arxiv_id":"2506.13983","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"An LLM-based system combining specification analysis, waveform analysis, and Monte Carlo Tree Self-Refine generates SystemVerilog assertions that outperform AssertLLM and ChIRAAG on I2C and RV-Timer designs.","lead":"SANGAM is a framework that uses LLM-guided Monte Carlo Tree Search to generate SystemVerilog assertions from hardware specifications, waveforms, and RTL. On two small designs it reports more formally verified assertions and higher coverage than two recent baselines.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The step from 'proven against RTL' to 'semantically correct' is unsupported; vacuous or true-but-irrelevant assertions could inflate every headline count.","rationale":"The paper's purpose is to show that SANGAM generates more and better assertions than prior LLM-based methods. For that claim to hold, the number of 'correct' assertions must reflect intended design behavior, not merely properties that happen to be true of the implementation. This is the least secure link in the argument. JasperGold's formal proof is necessary for syntactic and implementation-level correctness, but it cannot certify that an assertion captures the specification's intent. A formally proven assertion may be vacuous, trivially true, or irrelevant to the behaviors a verification engineer cares about. The Critic LLM is the only semantic filter, and its scores are uncalibrated and self-referential; there is no evidence that its notion of correctness matches human judgment. The paper itself routes final semantic assurance to a human engineer in Section III-C. Thus the headline claim that SANGAM generates 'twice the assertions' of prior methods is only as strong as the unverified semantic classification of the 152 and 46 assertions. The proposed audit is a concrete, feasible way to settle the concern: if most counted assertions satisfy criterion (a), the central claim survives; if many are vacuous or irrelevant, the claimed advantage shrinks. The reader's conditional verdict already captures this risk, so no change to the verdict is needed, but the condition should explicitly include a semantic audit rather than relying solely on formal proof counts.","tokens_in":9913,"tokens_out":4628,"duration_ms":55083,"concrete_test":"Run JasperGold vacuity checking on all 152 I2C and 46 RV-Timer assertions; then have two independent verification engineers, blinded to SANGAM's labels, classify each assertion against the original specification as (a) expresses intended behavior, (b) true but vacuous/trivial, or (c) unrelated/wrong, using a pre-registered rubric with inter-annotator agreement. If the fraction of (b)+(c) is large, or vacuity reports flag meaningful counts, the headline 'semantically correct' counts must be re-scaled and the comparison to baselines re-stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim in Section IV-B is that SANGAM produces '152 syntactically and semantically correct assertions' for I2C and 46 for RV-Timer, yielding large percentage improvements over AssertLLM and ChIRAAG. The only semantic gate is JasperGold formal verification against the same RTL, plus an LLM Critic score. Formal proof establishes that a property holds on all reachable states of the implementation, not that it expresses the specification's intended behavior. A property can be provable and still vacuous (antecedent never fires), trivially true, or only a narrow slice of intended behavior. The MCTS reward is the Critic LLM's self-score from -100 to 100, with no calibration against human judgment or a golden assertion set, so the search optimizes what the Critic likes rather than verification intent. Section III-C explicitly leaves 'manually verified by the Verification Engineer' as a step after the framework, conceding that semantic correctness is not established by the pipeline. The coverage numbers quantify exercised RTL behavior, not the fraction of intended behaviors captured. Because every headline count is filtered only by syntax and RTL validity, vacuous or true-but-irrelevant assertions could inflate the claimed advantage over both baselines.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces SANGAM, a three-stage framework that uses LLM agents (DeepSeek-R1) with a modified Monte Carlo Tree Self-Refine (MCTSr) algorithm to generate SystemVerilog assertions from multi-modal design specifications (text, architecture, waveforms). Stage 1 extracts signal-wise information via Signal Mapper, Spec Analyzer, and Waveform Analyzer agents; Stage 2 builds a reasoning tree per signal, using a Critic LLM and Cadence JasperGold syntax feedback to guide node expansion and reward; Stage 3 corrects syntax, deduplicates, and combines assertions. The authors evaluate on I2C and RV-Timer, reporting 152 and 46 syntactically correct assertions (204% and 254% improvements over AssertLLM and ChIRAAG, respectively) and branch/toggle/property coverage mostly above 74-100%. The central claim is that MCTS self-refine yields an extensive, high-quality set of formally verified assertions that better capture design intent than prior LLM-based methods.","tokens_in":10133,"tokens_out":4580,"duration_ms":49133,"significance":"If the results hold, SANGAM would make a useful contribution to LLM-based hardware assertion generation, achieving substantially larger sets of verified assertions than existing pipelines and demonstrating the viability of MCTS-guided self-refinement in this domain. The paper provides a concrete, reproducible pipeline (with code link), uses established benchmarks (AssertLLM and ChIRAAG RTL designs), and employs JasperGold for formal verification and coverage analysis, which are appropriate measurement tools. The coverage numbers and the explicit cost analysis are welcome concrete details. However, the significance is conditional: the headline counts and improvements rest on a semantic-correctness claim that is not adequately supported, and the central novelty (MCTS self-refine) is never isolated by an ablation, leaving the mechanism that drives the improvements unvalidated.","major_comments":[{"comment":"The claim that SANGAM produces '152 syntactically and semantically correct assertions' (I2C) and '46 syntactically and semantically correct assertions' (RV-Timer) is not supported by the evidence presented. Formal verification with JasperGold proves that each assertion holds on all reachable states of the given RTL implementation, but it does not establish that the assertion expresses the intended behavior from the specification. A property can be formally provable yet vacuous (antecedent never fires), trivially true, or only a narrow slice of the intended behavior. The paper itself, in Section III-C, states that the deduplicated assertions 'can be manually verified by the Verification Engineer against the specification to obtain the final correct set of assertions,' which concedes that the pipeline does not itself establish semantic correctness. The reported counts should be re-labeled as 'syntactically correct and formally verified against the RTL' pending a human semantic audit or comparison against a golden assertion set, and the headline percentage improvements should be recomputed accordingly.","section":"Section IV-B, 'Results and Discussion'"},{"comment":"The central novelty of the framework, the MCTS self-refine algorithm, is never isolated by any ablation. The only comparisons in Section IV are against AssertLLM and ChIRAAG, which are entirely different pipelines with different prompts, LLMs, and evaluation criteria. To support the claim that the MCTS self-refine component is responsible for the improved assertion counts and coverage, the authors should provide an ablation that runs the same Stage 1 and Stage 3 components with and without Stage 2 (for example, a single-pass SVA generation with the same prompts, or a greedy refinement loop without tree search). Without such an ablation, the 204% and 254% improvements cannot be attributed to the MCTS mechanism, and the paper's primary methodological contribution remains unverified.","section":"Section III-B, 'Stage 2: Assertion Generation'"},{"comment":"The baseline comparisons are not conducted in a common experimental harness. The AssertLLM and ChIRAAG assertion counts appear to be taken from their original publications (or from unstated settings), and the two designs are evaluated with different RTL sources and different evaluation criteria. The paper does not document the exact LLM versions, prompts, or JasperGold settings used for the baselines, nor does it rerun them with the same DeepSeek-R1 backbone and the same verification flow. Moreover, all reported results appear to come from a single run with fixed hyperparameters (n_rollouts = 4, c = 1.4), as described in Section IV-A. No variance, multiple seeds, or sensitivity analysis is provided, so the reported percentage improvements may be driven by stochasticity or configuration differences rather than by the method itself. The authors should either rerun the baselines in a common harness or clearly state and justify the source of the baseline numbers and the stability of their own results.","section":"Section IV-A and IV-B, 'Results and Discussion'"},{"comment":"The coverage analysis is presented as evidence that the generated assertions 'are more effective in capturing the design intent' and 'take a significant step toward completeness.' Coverage values, however, quantify which RTL structures are exercised or proved by the assertion set, not the fraction of intended behaviors from the specification that are captured. A set of assertions can achieve high toggle and branch coverage while omitting critical protocol semantics. The claim about 'design intent' is therefore not supported without a golden assertion set or a human semantic audit. Additionally, the numbers in Fig. 3 are ambiguous: the text states 'above 90% branch and toggle coverage and 74% property coverage,' but the figure appears to show both 100% and 74.82% values; please clarify which bar corresponds to which design and coverage type, and reconcile the text with the figure.","section":"Section IV-B, 'Results and Discussion', and Fig. 3"}],"minor_comments":[{"comment":"The phrase 'Back-propogation' in the heading should be 'Backpropagation.'","section":"Section III-B"},{"comment":"References [3] and [15] are the same MCTSr paper, and references [4] and [12] are the same AssertLLM paper; duplicate citations should be consolidated.","section":"References"},{"comment":"The formatting of Table II is unclear: the per-signal rows appear to list only SANGAM counts, while the ChIRAAG column only shows the total of 11. The caption says signal-wise results are not available for ChIRAAG, but the table layout implies a per-signal ChIRAAG column. Please restructure the table to make clear which numbers belong to which method.","section":"Table II"},{"comment":"The coverage bar chart lacks a legend or direct labeling of which bar corresponds to I2C versus RV-Timer and to branch/property/toggle coverage; the numeric labels are also not keyed to the legend in the text.","section":"Fig. 3"},{"comment":"The final manual verification step by a Verification Engineer is mentioned as an optional post-processing step, but the reported counts in Section IV-B are presented as final. Please state explicitly whether the 152 and 46 counts include any manual verification, and if not, adjust the terminology throughout the paper.","section":"Section III-C"},{"comment":"Minor wording: 'to divide the syntactically correct and incorrect assertions' should be 'to classify the assertions into syntactically correct and incorrect groups.'","section":"Section IV-A"}],"recommendation":"major_revision","confidential_remarks":"The paper's core idea is timely and the experimental setup (real RTL designs, JasperGold, cost analysis) is credible, but the current evaluation does not yet support the headline claims. The main risks are (1) the semantic-correctness inference from formal verification, (2) the lack of an ablation for the MCTS component, and (3) the non-common-harness baseline comparison. These are fixable with additional experiments (human audit or golden assertions, an MCTS ablation, a rerun of baselines, and multiple seeds). I therefore recommend major revision rather than rejection. The paper may benefit from the editor checking whether the duplicate references and unclear table/figure labeling are corrected during revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nHere's the quick read on arXiv:2506.13983 (SANGAM). The genuinely new piece is the combination: they take MCTSr, a known LLM self-refine search, and apply it to SVA generation per signal, adding a waveform-analyzer agent and feeding syntax feedback from JasperGold back into node expansion. That is a sensible engineering integration, and the paper documents prompts, cost, and design choices clearly. The empirical claim—152 'correct' assertions on I2C vs AssertLLM's 50, and 46 on RV-Timer vs ChIRAAG's 11—is concrete and the code is promised publicly.\n\nWhat it does well: it is not a toy; they use two real designs, check syntax with a commercial formal tool, and report branch/property/toggle coverage. The appendix prompts are useful for anyone trying to reproduce. The cost analysis (roughly $16 total) is a nice practical touch.\n\nThe soft spots are in the evaluation, and they are not minor. First, the counts in Table I/II are called 'syntactically and semantically correct' in Section IV-B, but the only semantic filter is JasperGold proving each property against the same RTL. A property can be provable and vacuous (antecedent never fires) or true-but-not-the-intended-behavior; the paper provides no golden assertion set and no human audit of the final deduplicated set. In fact, Section III-C explicitly says the final set 'can be manually verified by the Verification Engineer against the specification,' which concedes the pipeline itself does not establish semantic correctness. That overstates the headline result and the percentage improvements, since empty or trivial assertions would inflate counts.\n\nSecond, the central novelty—MCTS self-refine—is never isolated. There is no ablation comparing SANGAM to a single-pass version with the same agents and no tree search. Baselines are not rerun in a common harness; AssertLLM's outputs are not public, and ChIRAAG's signal-wise results are not available. All numbers appear to be single-run, with no error bars or variance. That leaves the load-bearing claim 'twice as many assertions' on a fairly soft footing, even though the direction is plausible.\n\nThe stress-test note from your desk lands: the step from 'proved against RTL' to 'semantically correct' is the weak link, and it is worth flagging to the authors.\n\nWho should read it: anyone working on LLM-based RTL verification will get value from the architecture and prompt designs. It deserves a serious referee, but the reviewer should ask for an ablation, a shared harness, and a human or golden-set semantic audit before the counts are taken at face value.\n\nMy verdict: send to peer review, expect heavy revision.","headline":"Plausible new integration of MCTSr for SVA generation, with useful prompts and concrete two-design results, but the 'semantically correct' counts are gated only by RTL validity and the MCTS component isn't ablated.","tokens_in":10692,"tokens_out":2018,"would_cite":false,"duration_ms":20409,"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":"SANGAM, a three-stage framework using Monte Carlo Tree Self-Refine, claims to generate over twice as many correct SystemVerilog assertions as state-of-the-art LLM methods, with 152 on I2C and 46 on RV-Timer.","keywords":["SystemVerilog assertions","Monte Carlo Tree Search","MCTSr","LLM-based verification","hardware assertion generation","formal verification","coverage analysis","specification understanding"],"falsifier":"Run SANGAM on the same I2C and RV-Timer specifications, then test every final assertion against a hand-written golden assertion set or against a mutated RTL where single bugs are injected: if the 152 and 46 assertions do not match the golden set or fail to catch injected bugs, the 'syntactically and semantically correct' label is not sufficient to establish that the framework captures design intent.","tokens_in":9686,"feed_emoji":"⚙️","tokens_out":11227,"duration_ms":102205,"temperature":0.7,"pith_summary":"This paper claims that adding a Monte Carlo Tree Self-Refine (MCTSr) search layer to LLM-based hardware verification can produce far more correct SystemVerilog assertions than existing single-pass or minimally iterative LLM tools. On the I2C design, SANGAM reports 152 syntactically and semantically correct assertions versus 50 for AssertLLM, a 204% increase; on a RISC-V timer it reports 46 versus 11 for ChIRAAG, a 254% increase. The framework processes multi-modal specifications into a signal-wise information bank, then grows a reasoning tree for each signal using critic feedback and formal-verification logs, and finally deduplicates the resulting assertion sets. If the reported verification and coverage numbers hold, SANGAM would make automated assertion generation substantially more complete, covering functional properties that prior methods miss while keeping API costs low ($16 total).","feed_headline":"Monte Carlo search more than doubles valid hardware assertions","feed_subtitle":"SANGAM reports 152 correct assertions on I2C and 46 on a RISC-V timer, outrunning prior LLM tools.","key_machinery":"The key machinery is the modified Monte Carlo Tree Self-Refine (MCTSr) search combined with a three-stage pipeline. Stage 1 uses three LLM agents (Signal Mapper, Spec Analyzer, Waveform Analyzer) to build a signal-wise information bank. Stage 2 runs a UCT-based tree search per signal: each node holds a set of assertions, and the selection score is $UCT_a = Q(a) + c\\sqrt{(\\ln(N(\\text{Father}(a))+1)/(N(a)+\\epsilon))}$, with greedy selection. Expansion generates a child node via an SVA-generation LLM fed with the current assertions, critic feedback, JasperGold syntax logs, and RAG context from assertion reference documents. Evaluation uses a critic LLM to assign a reward in $[-100,100]$, with scores above 95 suppressed and repeated sampling on revisits. Backpropagation updates a node as $Q'(a) = \\frac{1}{2}(Q(a) + \\max_{i \\in \\text{children}(a)} Q(i))$. Stage 3 unions all nodes, runs syntax correction, and deduplicates to produce the final set.","core_discovery":"The paper's central claim is that assertion generation should be treated as an explicit search over the space of possible assertion sets, not as a single LLM completion. SANGAM's modified MCTSr algorithm constructs, for each signal, a tree in which every node is a set of assertions; selection uses a UCT score, expansion produces a child node by combining critic feedback and JasperGold syntax logs with retrieval-augmented context, and evaluation assigns a critic score in [-100,100] with full-score suppression and resampling to reduce over-optimism. After four rollouts, all tree nodes are merged, syntax-corrected, and deduplicated to give the final assertion set. The outcome on the two benchmark designs is a claimed 152 correct assertions for I2C and 46 for RV-Timer, with both designs achieving above 90% branch and toggle coverage and 74% property coverage. The authors interpret this as evidence that iterative multi-path reasoning with tool feedback captures functional design intent more completely than the compared baselines.","pith_inferences":["The paper's own limitation statement concedes that inter-signal assertion irredundancy is not guaranteed; a natural next step is to run the same search over groups of related signals, though this would enlarge the tree and raise cost.","Formal verification against the RTL proves only that each assertion holds on that implementation, not that it expresses the intended specification; an independent audit against a hand-written golden assertion set would show whether the reported counts reflect semantic coverage or just volume.","A stronger evaluation of assertion quality would be mutation testing: inject buggy RTL variants and measure how many of the generated assertions fail on each mutant, which directly tests the assertions' ability to catch real errors.","The method's reliance on a commercial formal tool for syntax and feedback means the pipeline is tied to that toolchain; porting it to an open-source equivalent could change the reward signal and thereby the final assertion set."],"forward_implications":["If the numbers hold, verification engineers can start from a much larger candidate assertion set, shifting effort from authoring assertions to reviewing and pruning them.","The same MCTSr-with-tool-feedback pattern could be applied to other LLM-generated hardware artifacts, such as testbenches or coverage constraints, wherever a formal checker can supply feedback.","Because the total API cost is reported as $16 for both designs, the approach is cheap enough to run per block in a design flow, making completeness-oriented assertion generation practical.","The reported coverage gains suggest that MCTS-guided generation surfaces functional properties, such as the RISC-V timer's interrupt behavior, that single-shot methods miss."],"supporting_citations":[{"why":"Baseline ChIRAAG method for the RV-Timer design; SANGAM claims 46 correct assertions versus its 11.","marker":"[2]"},{"why":"AssertLLM method used as the I2C baseline in the signal-wise comparison; SANGAM claims 152 correct assertions versus its 50.","marker":"[12]"},{"why":"MCTSr algorithm, the base search procedure that SANGAM modifies with syntax feedback and formal-verification logs.","marker":"[15]"},{"why":"DeepSeek-R1, the LLM used to implement all the agents (Spec Analyzer, Signal Mapper, Waveform Analyzer, Critic, SVA generator, Corrector, Deduplicator).","marker":"[18]"},{"why":"Cadence JasperGold, the formal verification and coverage tool that provides syntax feedback, correctness proofs, and coverage results.","marker":"[19]"},{"why":"AssertLLM dataset, which supplies the I2C RTL used for formal verification of the generated assertions.","marker":"[23]"}],"fun_headline_variants":["SANGAM: MCTSr doubles valid hardware assertions","Monte Carlo self-refine yields 152 correct I2C SVAs","Tree search boosts assertion generation beyond LLM baselines","SANGAM's MCTSr outperforms prior tools on hardware specs","Assertion generation via MCTSr shows 2x valid output"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The evaluation assumes that an assertion formally proved against the RTL by JasperGold, and scored by the critic LLM, is a correct expression of the design's intended behavior; no independent golden assertion set or human semantic audit is used to confirm this.","fun_headline_variants_meta":{"raw":{"variants":["SANGAM: MCTSr doubles valid hardware assertions","Monte Carlo self-refine yields 152 correct I2C SVAs","Tree search boosts assertion generation beyond LLM baselines","SANGAM's MCTSr outperforms prior tools on hardware specs","Assertion generation via MCTSr shows 2x valid output"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000204,"raw_usage":{"total_tokens":1378,"prompt_tokens":919,"completion_tokens":459,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":535,"completion_tokens_details":{"reasoning_tokens":384}},"tokens_in":535,"tokens_out":459,"duration_ms":5624,"temperature":1.0,"reasoning_tokens":384,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T04:47:59.122657+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run SANGAM on the same I2C and RV-Timer specifications, then test every final assertion against a hand-written golden assertion set or against a mutated RTL where single bugs are injected: if the 152 and 46 assertions do not match the golden set or fail to catch injected bugs, the 'syntactically and semantically correct' label is not sufficient to establish that the framework captures design intent.","supporting_citations":[{"cited_title":"Chiraag: Chatgpt informed rapid and automated assertion generation,","cited_arxiv_id":null,"evidence_quote":"Baseline ChIRAAG method for the RV-Timer design; SANGAM claims 46 correct assertions versus its 11."},{"cited_title":"Assertllm: Generating hardware verification assertions from design specifications via multi-llms,","cited_arxiv_id":null,"evidence_quote":"AssertLLM method used as the I2C baseline in the signal-wise comparison; SANGAM claims 152 correct assertions versus its 50."},{"cited_title":"JasperGold,","cited_arxiv_id":null,"evidence_quote":"Cadence JasperGold, the formal verification and coverage tool that provides syntax feedback, correctness proofs, and coverage results."},{"cited_title":"Assertllm dataset: Generating hardware ver- ification assertions from design specifications via multi-llms,","cited_arxiv_id":null,"evidence_quote":"AssertLLM dataset, which supplies the I2C RTL used for formal verification of the generated assertions."}],"review_version":1}