Researchers Aim to Improve Reliability of EDA Tools with Fuzzing and Formal Verification

Researchers from a Computerphile video focus on improving the reliability of Electronic Design Automation (EDA) tools, which hardware engineers use to convert human-readable hardware designs into configurations for chips like FPGAs (Field Programmable Gate Arrays). Their work targets bugs in place-and-route tools, which position logic gates and establish connections on an FPGA, by employing fuzzing—a technique generating random hardware designs to test tool accuracy. Using an equivalence checker, they identified a critical bug where the tool incorrectly removed an inverter from a dynamically reconfigurable lookup table, assuming static table contents despite external reconfiguration signals. The team also explores formal verification, a mathematical approach to prove EDA tools function correctly, leveraging proof-assistant languages like Lean and Isabelle to automate and validate proofs. While formal verification is complex due to software scale, it aims to eliminate reliance on bug-finding methods by ensuring tools preserve design integrity. Their projects include building verified synthesis tools and equivalence checkers to reduce errors in hardware design workflows. The research highlights vulnerabilities in commercial, closed-source EDA tools and advocates for more robust verification techniques.