SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine

TL;DR

SANGAM is a novel framework that leverages Large Language Models and Monte Carlo Tree Search to automatically generate SystemVerilog Assertions from industry specifications, improving assertion quality and efficiency.

Contribution

It introduces a three-stage LLM-guided Monte Carlo Tree Search framework for automatic SVA generation from specifications, enhancing current assertion generation methods.

Findings

Outperforms recent assertion generation methods in evaluation

Generates robust and accurate SVAs from complex specifications

Demonstrates effectiveness of LLM-guided reasoning in hardware verification

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.