REVIEW 4 major objections 6 minor 23 references
SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine
T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read 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.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [Section IV-B, 'Results and Discussion'] 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 III-B, 'Stage 2: Assertion Generation'] 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 IV-A and IV-B, 'Results and Discussion'] 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 IV-B, 'Results and Discussion', and Fig. 3] 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.
minor comments (6)
- [Section III-B] The phrase 'Back-propogation' in the heading should be 'Backpropagation.'
- [References] References [3] and [15] are the same MCTSr paper, and references [4] and [12] are the same AssertLLM paper; duplicate citations should be consolidated.
- [Table II] 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.
- [Fig. 3] 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 III-C] 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 IV-A] Minor wording: 'to divide the syntactically correct and incorrect assertions' should be 'to classify the assertions into syntactically correct and incorrect groups.'
Circularity Check
No significant circularity; SANGAM's headline counts are checked by an external formal tool and published baselines, and the semantic-correctness overclaim is a validity caveat rather than a circular derivation.
full rationale
The load-bearing empirical claims (assertion counts in Tables I and II, coverage in Fig. 3) are checked against external artifacts: Cadence JasperGold, the AssertLLM I2C RTL, the ChIRAAG RV-Timer RTL, and the published AssertLLM/ChIRAAG counts. The MCTSr reward is an LLM critic score, but no parameter is fitted to the reported counts, and the final counts are produced by an independent formal tool rather than by the critic. The framework's internal use of JasperGold for syntax feedback and final verification does not make the counts definitional: syntax and proof-against-RTL are external properties of the generated assertions, not inputs to the pipeline. The genuine weakness is the wording in Section IV-B, where formally verified assertions are called 'syntactically and semantically correct'; formal proof against an implementation does not establish specification-level semantic intent, and Section III-C itself concedes that the final set 'can be manually verified by the Verification Engineer against the specification to obtain the final correct set of assertions.' This is a correctness and reporting caveat, not a circular derivation. ChIRAAG [2] is a self-citation with overlapping authors, but it serves only as a comparison baseline and does not justify SANGAM's central mechanism. No equation or fitting step reduces to its own input, so no circularity is found.
Assumptions & free parameters
free parameters (3)
- MCTS exploration constant c =
1.4
- Number of MCTS rollouts n_rollouts =
4
- Critic score suppression threshold =
95
assumptions (4)
- domain assumption The LLM critic's numerical score, resampled and backpropagated via Q'(a)=0.5*(Q(a)+max_child Q), is a reliable reward signal for assertion quality.
- domain assumption Assertions that pass JasperGold formal verification against the RTL are 'syntactically and semantically correct' and capture design intent.
- domain assumption The RTL used for I2C and RV-Timer is a faithful implementation of the specifications that the LLMs analyze.
- domain assumption Waveform analysis improves assertion generation.
Cite this review
Pith. "Pith review of SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine." pith.science (2026). https://pith.science/paper/GIXXY5MT
@misc{pith2026250613983,
author = {Pith},
title = {Pith review of: SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine},
year = {2026},
howpublished = {\url{https://pith.science/paper/GIXXY5MT}},
note = {Machine review of arXiv:2506.13983}
}
read the original abstract
Recent advancements in the field of reasoning using Large Language Models (LLMs) have created new possibilities for more complex and automatic Hardware Assertion Generation techniques. This paper introduces SANGAM, a SystemVerilog Assertion Generation framework using LLM-guided Monte Carlo Tree Search for the automatic generation of SVAs from industry-level specifications. The proposed framework utilizes a three-stage approach: Stage 1 consists of multi-modal Specification Processing using Signal Mapper, SPEC Analyzer, and Waveform Analyzer LLM Agents. Stage 2 consists of using the Monte Carlo Tree Self-Refine (MCTSr) algorithm for automatic reasoning about SVAs for each signal, and finally, Stage 3 combines the MCTSr-generated reasoning traces to generate SVA assertions for each signal. The results demonstrated that our framework, SANGAM, can generate a robust set of SVAs, performing better in the evaluation process in comparison to the recent methods.
Figures
Figures from the paper (4 more)
Reference graph
Works this paper leans on
-
[1]
Llm-assisted generation of hardware assertions,
R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “Llm-assisted generation of hardware assertions,”arXiv preprint, vol. arXiv:2306.14027, 2023
arXiv 2023
-
[2]
Chiraag: Chatgpt informed rapid and automated assertion generation,
B. Mali, K. Maddala, V . Gupta, S. Reddy, C. Karfa, and R. Karri, “Chiraag: Chatgpt informed rapid and automated assertion generation,” inISVLSI, 2024, pp. 680–683
work page 2024
-
[4]
W. Fang, M. Li, M. Li, Z. Yan, S. Liu, Z. Xie, and H. Zhang, “Assertllm: Generating and evaluating hardware verification assertions from design specifications via multi-llms,”arXiv preprint, vol. arXiv:2402.00386, 2024
arXiv 2024
-
[5]
Global Large Language Model (LLM) Research Re- port 2024-2030,
GlobeNewswire, “Global Large Language Model (LLM) Research Re- port 2024-2030,” https://tinyurl.com/LLMReport, 2024
work page 2024
-
[6]
Hlspilot: Llm-based high-level synthesis,
C. Xiong, C. Liu, H. Li, and X. Li, “Hlspilot: Llm-based high-level synthesis,”arXiv preprint arXiv:2408.06810, 2024
arXiv 2024
-
[7]
Lhs: Llm assisted efficient high-level synthesis of deep learning tasks,
E. B. E. Reddy, S. Bhattacharyya, A. Sarmah, F. Nongpoh, K. Maddala, and C. Karfa, “Lhs: Llm assisted efficient high-level synthesis of deep learning tasks,”ACM TODAES, 2025
work page 2025
-
[8]
Large language model (llm) for standard cell layout design optimization,
C.-T. Ho and H. Ren, “Large language model (llm) for standard cell layout design optimization,” inLAD, 2024, pp. 1–6
work page 2024
-
[9]
Automatically improving llm-based verilog generation using eda tool feedback,
J. Blocklove, S. Thakur, B. Tan, H. Pearce, S. Garg, and R. Karri, “Automatically improving llm-based verilog generation using eda tool feedback,”ACM TODAES, 2025
work page 2025
Show all 23 references
-
[10]
Vhdl-eval: A framework for evaluating large language models in vhdl code generation,
P. Vijayaraghavan, L. Shi, S. Ambrogio, C. Mackin, A. Nitsure, D. Beymer, and E. Degan, “Vhdl-eval: A framework for evaluating large language models in vhdl code generation,” in2024 IEEE LLM Aided Design Workshop (LAD). IEEE, 2024, pp. 1–6
2024
-
[11]
Layoutcopilot: An llm-powered multi-agent collaborative framework for interactive analog layout design,
B. Liu, H. Zhang, X. Gao, Z. Kong, X. Tang, Y . Lin, R. Wang, and R. Huang, “Layoutcopilot: An llm-powered multi-agent collaborative framework for interactive analog layout design,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2025
2025
-
[12]
Assertllm: Generating hardware verification assertions from design specifications via multi-llms,
W. Fang, M. Li, M. Li, Z. Yan, S. Liu, H. Zhang, and Z. Xie, “Assertllm: Generating hardware verification assertions from design specifications via multi-llms,” inLAD, 2024
2024
-
[13]
(security) assertions by large language models,
R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “(security) assertions by large language models,”IEEE TIPS, vol. 19, pp. 4374–4389, 2024
2024
-
[14]
A survey of monte carlo tree search methods,
C. B. Browne, E. Powley, D. Whitehouse, S. M. Lucas, P. I. Cowling, P. Rohlfshagen, S. Tavener, D. Perez, S. Samothrakis, and S. Colton, “A survey of monte carlo tree search methods,”IEEE Transactions on Computational Intelligence and AI in games, vol. 4, no. 1, pp. 1–43, 2012
2012
-
[15]
Accessing gpt-4 level mathematical olympiad solutions via monte carlo tree self-refine with llama-3 8b,
D. Zhang, X. Huang, D. Zhou, Y . Li, and W. Ouyang, “Accessing gpt-4 level mathematical olympiad solutions via monte carlo tree self-refine with llama-3 8b,”arXiv preprint arXiv:2406.07394, 2024
2024 arXiv
-
[16]
Improve mathematical reasoning in lan- guage models by automated process supervision,
L. Luo, Y . Liu, R. Liu, S. Phatale, H. Lara, Y . Li, L. Shu, Y . Zhu, L. Meng, J. Sunet al., “Improve mathematical reasoning in lan- guage models by automated process supervision,”arXiv preprint arXiv:2406.06592, vol. 2, 2024
2024 arXiv
-
[17]
Interpretable contrastive monte carlo tree search reasoning,
Z. Gao, B. Niu, X. He, H. Xu, H. Liu, A. Liu, X. Hu, and L. Wen, “Interpretable contrastive monte carlo tree search reasoning,”arXiv preprint arXiv:2410.01707, 2024
2024 arXiv
-
[18]
Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning,
W. Liang and D. Team, “Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning,” January 2025, https://arxiv.org/abs/2412.16720
2025 arXiv
-
[19]
JasperGold,
Cadence, “JasperGold,” https://www.cadence.com/en US/home/tools/ systemdesignand-verification/formal-and-static-verification.html, 2025
2025
-
[20]
Dasgupta,A Roadmap for Formal Property Verification
P. Dasgupta,A Roadmap for Formal Property Verification. Dordrecht: Springer, 2006
2006
-
[21]
A. B. Mehta,SystemVerilog Assertions and Functional Coverage: Guide to Language, Methodology and Applications. New York: Springer, 2013
2013
-
[22]
Vijayaraghavan and M
S. Vijayaraghavan and M. Ramanathan,A Practical Guide for Sys- temVerilog Assertions. Boston, MA: Springer, 2005
2005
-
[23]
Assertllm dataset: Generating hardware ver- ification assertions from design specifications via multi-llms,
Z. Yaoet al., “Assertllm dataset: Generating hardware ver- ification assertions from design specifications via multi-llms,” https://github.com/hkust-zhiyao/AssertLLM, 2024. 7 APPENDIXA CUSTOMINSTRUCTIONS [System Prompt for Signal Mapper] • Please act as a signal name mapping t...
2024
-
[100]
• Be very strict, ensureCORRECTNESS,CONSISTENCY, andCOMPLETENESSof the SV As
Also focus on Clock Cycle Misinterpretations, and nested if-else and long conditions. • Be very strict, ensureCORRECTNESS,CONSISTENCY, andCOMPLETENESSof the SV As. Focus on these three things while grading the SV As and providing feedback. • Let’s think step by step. Fig. 6: S...
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.