Equivalence Checking Reveals, Assertions Clarify

Simulation-based testbenches are still the norm when it comes to assessing the correct functionality of Register Transfer Level (RTL) designs generated by Large Language Models (LLMs). That is not enough: a minimal simulation trace can easily hide design flaws. Moreover, automatically scaling such benchmarks for large designs becomes infeasible. The field is already moving towards a formal, and more easily scalable method in the form of Logical Equivalence Checking (LEC) for that reason. LEC is the right next step, but it only says whether two netlists match, whether they are equal or not. LEC against the reference can be too restrictive, penalising LLM code for not matching microarchitectural details, even if no specification requirements are broken. We show that Formal Property Verification (FPV) with SystemVerilog Assertions (SVA) can sit next to LEC and more precisely name the broken behaviour---e.g., handshake, sequencing, or datapath, providing us with more insights on the shortcomings of LLM-generated RTL. On public GPT-3.5 and GPT-4 generation samples from the RTLLM paper, tested with the latest released testbenches and the same LEC flow used by NotSoTiny, 93 samples pass the testbench, 35 of those fail LEC, and 25 of those 35 fail a reference-proven assertion, totalling 32 assertion fails. Namely, for all RTLLM designs for which LEC detects a false positive, there is at least one assertion which is proven in the golden reference and fails in a sample like LEC does. Furthermore, we demonstrate how FPV is more adaptable and better at checking specification requirements, rather than reference RTL similarity.