Finding Hardware Bugs - Computerphile

The research team is focused on improving the reliability of Electronic Design Automation (EDA) tools, which hardware engineers use to create hardware. These tools take a human-readable hardware design and transform it through a sequence of processes, such as elaboration, synthesis, and place-and-route, ultimately producing a configuration file for chips like FPGAs. FPGAs are unique because their functionality can be reprogrammed after manufacturing, unlike fixed-function ASICs or general-purpose CPUs that rely on software instructions. The core problem addressed is trusting these EDA tools. The concern isn't about malicious intent, but rather the potential for bugs within the tools themselves. A bug in an EDA tool can lead to errors in the hardware design, which are notoriously difficult to debug. The research specifically targets bugs in place-and-route tools. To find these bugs, the team employed a technique called fuzzing. This involves generating a large number of random, yet superficially valid, hardware designs. These designs are then fed into the place-and-route tool. The output is then compared to the input using an equivalence checker, another EDA tool. If the equivalence checker detects a discrepancy, it indicates a potential bug. Due to the commercial and closed-source nature of most EDA tools, direct access to their source code is typically not possible. Therefore, the primary method for understanding a bug is to minimize the design that triggers it, reducing it to a small, core example that still exhibits the erroneous behavior. This minimized design can then be filed as a bug report to the tool vendors. One specific bug found involved a lookup table (LUT) within an FPGA. The design requested row one of the LUT, and an inverter was present in the input path. The place-and-route tool, in an effort to optimize, noticed that row one contained the same data as row zero. It then removed the inverter and directly supplied zero to the input, assuming the output would remain the same. However, this particular LUT had an additional port for reconfiguration. The place-and-route tool failed to recognize that this reconfiguration port was constantly active, meaning the LUT's contents were being dynamically updated. Consequently, while removing the inverter was safe for the initial configuration, it became incorrect once the LUT was reconfigured, leading to a functional error. The researchers believe there is significant scope for continued study of EDA tools and the development of new bug-finding techniques. Concurrently, they are exploring the concept of building inherently bug-free EDA tools through formal verification. This approach aims to create mathematical proofs demonstrating that the software (and by extension, the EDA tool) will always perform as intended, much like proving a mathematical theorem. Formal verification contrasts with the current software development practice of extensive testing. The challenge lies in translating complex software into mathematical theorems, which can be enormous due to the need to capture the program's source code, the programming language's semantics, and the underlying hardware. However, the proving process, while difficult, is not as conceptually deep as proving theorems like Fermat's Last Theorem. To manage this complexity, computer-aided proof systems, such as Lean, Coq, and Isabelle, are employed. These systems act as programming languages for mathematical proofs, allowing computers to assist in writing and verifying proofs by handling tedious details and checking for correctness. The ultimate goal is to use these formal methods to build verified EDA tools, making bug-finding techniques like fuzzing less necessary in the future. The fuzzer generates random, but deterministic, programs that can be processed by standard compilers like GCC and Clang.