-
SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine
Authors:
Adarsh Gupta,
Bhabesh Mali,
Chandan Karfa
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 u…
▽ More
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.
△ Less
Submitted 11 June, 2025;
originally announced June 2025.
-
LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification
Authors:
Karthik Maddala,
Bhabesh Mali,
Chandan Karfa
Abstract:
Writing SystemVerilog Assertions (SVA) is an important but complex step in verifying Register Transfer Level (RTL) designs. Conventionally, experts need to understand the design specifications and write the SVA assertions, which is time-consuming and error-prone. However, with the recent advancement of transformer models, the Large Language Models (LLMs) assisted assertion generation for design ve…
▽ More
Writing SystemVerilog Assertions (SVA) is an important but complex step in verifying Register Transfer Level (RTL) designs. Conventionally, experts need to understand the design specifications and write the SVA assertions, which is time-consuming and error-prone. However, with the recent advancement of transformer models, the Large Language Models (LLMs) assisted assertion generation for design verification is gaining interest in recent times. Motivated by this, we proposed a novel LLM-based framework, LAAG-RV, to generate SVA from the natural language specifications of the design. Our framework provides a one-time Verilog loop for signal synchronization in the generated SVA to improve the generated assertion quality. For our experiments, we created a custom LLM based on OpenAI GPT-4. Furthermore, we developed test cases to validate the LLM-generated assertions. Initial observations show that some generated assertions contain issues and did not pass all the test cases. However, by iteratively prompting the LLMs using carefully crafted manual prompts derived from test case failures in a simulator, the framework can generate correct SVAs. Our results on OpenTitan designs demonstrate that LLMs significantly simplify the process of generating assertions, making it efficient and less error-prone.
△ Less
Submitted 13 August, 2024;
originally announced September 2024.
-
MaskedHLS: Domain-Specific High-Level Synthesis of Masked Cryptographic Designs
Authors:
Nilotpola Sarma,
Anuj Singh Thakur,
Chandan Karfa
Abstract:
The design and synthesis of masked cryptographic hardware implementations that are secure against power side-channel attacks (PSCAs) in the presence of glitches is a challenging task. High-Level Synthesis (HLS) is a promising technique for generating masked hardware directly from masked software, offering opportunities for design space exploration. However, conventional HLS tools make modification…
▽ More
The design and synthesis of masked cryptographic hardware implementations that are secure against power side-channel attacks (PSCAs) in the presence of glitches is a challenging task. High-Level Synthesis (HLS) is a promising technique for generating masked hardware directly from masked software, offering opportunities for design space exploration. However, conventional HLS tools make modifications that alter the guarantee against PSCA security via masking, resulting in an insecure RTL. Moreover, existing HLS tools can't place registers at designated places and balance parallel paths in a cryptographic design which is needed to stop glitch propagation. This paper introduces a domain-specific HLS approach tailored to obtain a PSCA secure masked hardware implementation directly from a masked software implementation. It places the registers at specific locations required by the glitch-robust masking gadgets, resulting in a secure RTL. Moreover, our tool automatically balances parallel paths and facilitates a reduction in latency while preserving the PSCA security guaranteed by masking. Experimental results with the PRESENT Cipher's S-box and AES Canright's S-box masked with four state-of-the-art gadgets, show that MaskedHLS produces RTLs with 73.9% decrease in registers and 45.7% decrease in latency on an average} compared to manual register insertions. The PSCA security of the MaskedHLS generated RTLs is also shown with TVLA test.
△ Less
Submitted 16 July, 2024;
originally announced July 2024.
-
ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
Authors:
Bhabesh Mali,
Karthik Maddala,
Vatsal Gupta,
Sweeya Reddy,
Chandan Karfa,
Ramesh Karri
Abstract:
System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG…
▽ More
System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA from natural language specifications of a design. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we used few test cases to validate the LLM-generated assertions. Automatic feedback of log messages from the simulation tool to the LLM ensures that the framework can generate correct SVAs. In our experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations based on the simulation log. Our results on OpenTitan designs show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.
△ Less
Submitted 28 June, 2024; v1 submitted 31 January, 2024;
originally announced February 2024.
-
Benchmarking at the Frontier of Hardware Security: Lessons from Logic Locking
Authors:
Benjamin Tan,
Ramesh Karri,
Nimisha Limaye,
Abhrajit Sengupta,
Ozgur Sinanoglu,
Md Moshiur Rahman,
Swarup Bhunia,
Danielle Duvalsaint,
R. D.,
Blanton,
Amin Rezaei,
Yuanqi Shen,
Hai Zhou,
Leon Li,
Alex Orailoglu,
Zhaokun Han,
Austin Benedetti,
Luciano Brignone,
Muhammad Yasin,
Jeyavijayan Rajendran,
Michael Zuzak,
Ankur Srivastava,
Ujjwal Guin,
Chandan Karfa,
Kanad Basu
, et al. (11 additional authors not shown)
Abstract:
Integrated circuits (ICs) are the foundation of all computing systems. They comprise high-value hardware intellectual property (IP) that are at risk of piracy, reverse-engineering, and modifications while making their way through the geographically-distributed IC supply chain. On the frontier of hardware security are various design-for-trust techniques that claim to protect designs from untrusted…
▽ More
Integrated circuits (ICs) are the foundation of all computing systems. They comprise high-value hardware intellectual property (IP) that are at risk of piracy, reverse-engineering, and modifications while making their way through the geographically-distributed IC supply chain. On the frontier of hardware security are various design-for-trust techniques that claim to protect designs from untrusted entities across the design flow. Logic locking is one technique that promises protection from the gamut of threats in IC manufacturing. In this work, we perform a critical review of logic locking techniques in the literature, and expose several shortcomings. Taking inspiration from other cybersecurity competitions, we devise a community-led benchmarking exercise to address the evaluation deficiencies. In reflecting on this process, we shed new light on deficiencies in evaluation of logic locking and reveal important future directions. The lessons learned can guide future endeavors in other areas of hardware security.
△ Less
Submitted 11 June, 2020;
originally announced June 2020.
-
A Quick Introduction to Functional Verification of Array-Intensive Programs
Authors:
Kunal Banerjee,
Chandan Karfa
Abstract:
Array-intensive programs are often amenable to parallelization across many cores on a single machine as well as scaling across multiple machines and hence are well explored, especially in the domain of high-performance computing. These programs typically undergo loop transformations and arithmetic transformations in addition to parallelizing transformations. Although a lot of effort has been inves…
▽ More
Array-intensive programs are often amenable to parallelization across many cores on a single machine as well as scaling across multiple machines and hence are well explored, especially in the domain of high-performance computing. These programs typically undergo loop transformations and arithmetic transformations in addition to parallelizing transformations. Although a lot of effort has been invested in improving parallelizing compilers, experienced programmers still resort to hand-optimized transformations which is typically followed by careful tuning of the transformed program to finally obtain the optimized program. Therefore, it is critical to verify that the functional correctness of an original sequential program is not sacrificed during the process of optimization. In this paper, we cover important literature on functional verification of array-intensive programs which we believe can be a good starting point for one interested in this field.
△ Less
Submitted 22 May, 2019;
originally announced May 2019.
