Automated Testing, Verification and Repair of RTL Hardware Designs
Kevin Laeufer
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2024-157
August 4, 2024
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-157.pdf
All modern marvels of computer technology are built on microchips - grains of sand turned into computational components. Over more than five decades, we have seen rapid progress in computing performance, primarily thanks to semiconductor technology improvements that lowered power consumption and raised clock speeds. Recently, progress has stalled, and general-purpose hardware can no longer keep up with rising computational demands. Specialized hardware is the only way. Low-volume specialization is often not profitable, though, because chips are too expensive to design. While modern software developers have access to tools that allow them to innovate rapidly, hardware design tools are difficult to access and use. For this thesis, I investigated how ideas from modern software engineering can be applied to the hardware design domain. <br> Inspired by work on software compilers, I developed a new approach for adding coverage feedback to hardware designs such that many different simulators can be targeted with minimal effort. I built the RFUZZ tool, which uses coverage feedback to generate new test inputs, taking inspiration from work on mutational fuzz testing for software. I added support for formal verification to the open-source ChiselTest library, focusing on accessibility for new users. Finally, I designed the RTL-Repair tool, which automatically generates plausible repairs from a buggy hardware description and a failing test case through a combination of formal methods and simulation. <br> All four projects illustrate how we can improve the state-of-the-art hardware testing, verification, and debugging tools by integrating with the open-source ecosystem and applying a compiler engineering mindset. This approach has allowed me to quickly build superior coverage feedback and formal verification infrastructure for the new Chisel hardware language. It has also enabled the first hardware fuzzer, RFUZZ, which spawned a new line of research on hardware fuzzing, and the RTL-Repair tool, which provides correct repairs within seconds, several orders of magnitude faster than prior work.
Advisors: Koushik Sen
BibTeX citation:
@phdthesis{Laeufer:EECS-2024-157, Author= {Laeufer, Kevin}, Title= {Automated Testing, Verification and Repair of RTL Hardware Designs}, School= {EECS Department, University of California, Berkeley}, Year= {2024}, Month= {Aug}, Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-157.html}, Number= {UCB/EECS-2024-157}, Abstract= {All modern marvels of computer technology are built on microchips - grains of sand turned into computational components. Over more than five decades, we have seen rapid progress in computing performance, primarily thanks to semiconductor technology improvements that lowered power consumption and raised clock speeds. Recently, progress has stalled, and general-purpose hardware can no longer keep up with rising computational demands. Specialized hardware is the only way. Low-volume specialization is often not profitable, though, because chips are too expensive to design. While modern software developers have access to tools that allow them to innovate rapidly, hardware design tools are difficult to access and use. For this thesis, I investigated how ideas from modern software engineering can be applied to the hardware design domain. <br> Inspired by work on software compilers, I developed a new approach for adding coverage feedback to hardware designs such that many different simulators can be targeted with minimal effort. I built the RFUZZ tool, which uses coverage feedback to generate new test inputs, taking inspiration from work on mutational fuzz testing for software. I added support for formal verification to the open-source ChiselTest library, focusing on accessibility for new users. Finally, I designed the RTL-Repair tool, which automatically generates plausible repairs from a buggy hardware description and a failing test case through a combination of formal methods and simulation. <br> All four projects illustrate how we can improve the state-of-the-art hardware testing, verification, and debugging tools by integrating with the open-source ecosystem and applying a compiler engineering mindset. This approach has allowed me to quickly build superior coverage feedback and formal verification infrastructure for the new Chisel hardware language. It has also enabled the first hardware fuzzer, RFUZZ, which spawned a new line of research on hardware fuzzing, and the RTL-Repair tool, which provides correct repairs within seconds, several orders of magnitude faster than prior work.}, }
EndNote citation:
%0 Thesis %A Laeufer, Kevin %T Automated Testing, Verification and Repair of RTL Hardware Designs %I EECS Department, University of California, Berkeley %D 2024 %8 August 4 %@ UCB/EECS-2024-157 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-157.html %F Laeufer:EECS-2024-157