Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification

Ramesh Krishnamurthy, Danial Chitnis, Themis Prodromakis

Large language model (LLM) based assertion generation is making formal verification more accessible for Register Transfer Level (RTL) designs, but three practical issues remain. Ge…