ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

• URL: http://arxiv.org/abs/2402.00093v3
• Date: Fri, 28 Jun 2024 17:46:19 GMT
• Title: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
• Authors: Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, Ramesh Karri,
• Abstract summary: ChIRAAG, based on OpenAI GPT4, generates System Verilog Assertion (SVA) from natural language specifications of a design. In experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations. Our results show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification.
• Score: 10.503097140635374
• License: http://creativecommons.org/licenses/by/4.0/
• 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, 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.

Related papers

• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• A test suite of prompt injection attacks for LLM-based machine translation [4.459306403129608]
  LLM-based NLP systems typically work by embedding their input data into prompt templates which contain instructions and/or in-context examples. Recently, Sun and Miceli-Barone proposed a class of PIAs against LLM-based machine translation. We extend this approach to all the language pairs of the WMT 2024 General Machine Translation task.
  arXiv  Detail & Related papers  (2024-10-07T14:01:20Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  We present a novel benchmark to evaluate Large-Language Models' effectiveness for assertion generation. AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM.
  arXiv  Detail & Related papers  (2024-06-26T14:47:28Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  We introduce AutoIF, the first scalable and reliable method for automatically generating instruction-following training data. AutoIF transforms the validation of instruction-following data quality into code verification.
  arXiv  Detail & Related papers  (2024-06-19T13:29:53Z)
• DALD: Improving Logits-based Detector without Logits from Black-box LLMs [56.234109491884126]
  Large Language Models (LLMs) have revolutionized text generation, producing outputs that closely mimic human writing. We present Distribution-Aligned LLMs Detection (DALD), an innovative framework that redefines the state-of-the-art performance in black-box text detection. DALD is designed to align the surrogate model's distribution with that of unknown target LLMs, ensuring enhanced detection capability and resilience against rapid model iterations.
  arXiv  Detail & Related papers  (2024-06-07T19:38:05Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  This paper presents a new approach for scaling LLM assessment in translating formal syntax to natural language. We use context-free grammars (CFGs) to generate out-of-distribution datasets on the fly. We also conduct an assessment of several SOTA closed and open-source LLMs to showcase the feasibility and scalability of this paradigm.
  arXiv  Detail & Related papers  (2024-03-27T08:08:00Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  We introduce a novel task, Counterfactual Logical Modification (CLOMO), and a high-quality human-annotated benchmark. In this task, LLMs must adeptly alter a given argumentative text to uphold a predetermined logical relationship. We propose an innovative evaluation metric, the Self-Evaluation Score (SES), to directly evaluate the natural language output of LLMs.
  arXiv  Detail & Related papers  (2023-11-29T08:29:54Z)
• Mitigating Large Language Model Hallucinations via Autonomous Knowledge Graph-based Retrofitting [51.7049140329611]
  This paper proposes Knowledge Graph-based Retrofitting (KGR) to mitigate factual hallucination during the reasoning process. Experiments show that KGR can significantly improve the performance of LLMs on factual QA benchmarks.
  arXiv  Detail & Related papers  (2023-11-22T11:08:38Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  Large Language Models (LLMs) have shown success in code analysis and synthesis. We present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis.
  arXiv  Detail & Related papers  (2023-11-07T05:47:47Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  This paper presents ReEval, an LLM-based framework using prompt chaining to perturb the original evidence for generating new test cases. We implement ReEval using ChatGPT and evaluate the resulting variants of two popular open-domain QA datasets. Our generated data is human-readable and useful to trigger hallucination in large language models.
  arXiv  Detail & Related papers  (2023-10-19T06:37:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.