ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

要約

System Verilog Assertion (SVA) の定式化 — 重要かつ複雑なタスクは、Assertion Based Verification (ABV) プロセスの前提条件です。
従来、SVA の定式化には専門家による仕様の解釈が含まれており、時間がかかり、人的ミスが発生しやすくなっています。
最近、LLM に基づいたアサーションの自動生成が注目を集めています。
私たちは、OpenAI GPT4 に基づいて、設計の自然言語仕様から SVA を生成するための ChIRAAG と呼ばれる新しいフレームワークを設計しました。
ChIRAAG は、設計仕様を標準化された形式に系統的に分割し、LLM を使用して形式化された仕様からアサーションをさらに生成します。
さらに、LLM によって生成されたアサーションを検証するために、いくつかのテスト ケースを使用しました。
シミュレーション ツールから LLM へのログ メッセージの自動フィードバックにより、フレームワークが正しい SVA を生成できるようになります。
私たちの実験では、LLM で生成された生のアサーションのうち 27% のみにエラーがあり、シミュレーション ログに基づいて数回の反復で修正されました。
OpenTitan 設計に関する私たちの結果は、LLM がアサーション生成プロセスを合理化し、エンジニアを支援し、検証ワークフローを再構築できることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google