FormalEval: A Method for Automatic Evaluation of Code Generation via Large Language Models

One of the promising applications of Large Language Models (LLMs) is code generation. However, evaluating the quality of the generated code poses a significant challenge. Existing evaluation methods such as Rouge or HumanEval have limitations in terms of accuracy or efficiency. In this paper, we propose a formal evaluation method called FormalEval, which automates the process of checking generated code without the need for manual test case curation. We evaluated our method on common tasks related to Register-Transistor-Level (RTL) Verilog and SystemVerilog Assertions (SVA) generation in the field of Electronic Design Automation (EDA). Our method not only identifies 23 % of evaluation error in existing RTL benchmarking dataset, but also fixes the error via test case augmentation. We show FormalEval can help to identify better LLM prompting techniques on SVA generation task. Our method demonstrates state-of-the-art accuracy on the testing dataset.