Formal Verification of Hardware Designs from Large Language Models

Joshua Joseph Undergraduate Student Researcher

Primary Research Question: What are the shortcomings of Large Language Model generated hardware designs in comparison already verified designs?

The growing interest in Artificial Intelligence in commercial spaces has increased the demand for more reliable output from AI. Usually, Large Language Models(LLMs) require users to verify its output’s feasibility before applying it within a space. Applying formal methods to verify outputs based on specified metrics will increase the accuracy of LLMs and reduce the burden of verification of the user. This project explores LLM-generated hardware designs in Verilog and C and compares them to already verified designs across a variety of metrics. Particularly, hardware that has applications within safety-critical missions as mistakes are detrimental. These results will give insight into LLM’s decision-making, showcase the shortcomings of AI-generated hardware design, and provide a heading for what challenges need to be overcome in the AI formal verification space.