-
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, resha** 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.
