../

Domain-Adapted LLMs for VLSI Design and Verification: A Case Study on Formal Verification


Year
2024
Authors
Mingjie Liu, Minwoo Kang, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren
DOI
10.1109/VTS60656.2024.10538589

Related

Persistent Notes

In-text annotations

“Our results indicate that the largest and most capable models, such as GPT-4, are able to generate syntactically correct SVA implementations, yet there exists room for improvement in ensuring precise reflection of user intent given as high-level natural language descriptions of formal properties." Page 1

“For scalable and quantitative evaluation of various models, we devise a suite of multiple-choice question-answer (MCQA) benchmarks for a set of EDA-specific tasks, similar in format to established LLM benchmarks such as MMLU” Page 2

“As a preliminary case study, we first formulate a straightforward task of translating a natural language (NL) description of a formal property into concrete SystemVerilog Assertion syntax." Page 3

“Therefore, we first create an evaluation benchmark for the task of NL description to SVA code generation." Page 3

“Overall, our benchmark draws from 13 different testbenches and consist of a total of 81 human-crafted reference assertions." Page 3

%% Import Date: 2026-07-11T15:40:05.995-04:00 %%