Tutorial 9: Pre-silicon Verification & Post-Silicon Validation: An End-to-End Approach with Industrial Applications
Clark Barrett - Stanford Univ., Stanford, CA Wolfgang Ecker - Infineon Technologies AG , Munich, Germany Subhasish Mitra - Stanford Univ., Stanford, CA
Clark Barrett - Stanford Univ., Stanford, CA
This tutorial presents an end-to-end approach for pre-silicon verification and post-silicon validation of digital systems. In addition, it will also provide a unique hands-on experience on how to detect and localize difficult bugs automatically during pre-silicon verification and post-silicon validation. Several industrial case studies (from Intel, AMD, Freescale/NXP) will be covered, with special emphasis on practical experience of using these methodologies for pre-silicon verification of safety-critical automotive processor designs at Infineon.
The end-to-end principles will be based on recent approaches: Quick Error Detection (QED) technique for post-silicon validation and debug and Symbolic QED for pre-silicon verification. QED drastically reduces error detection latency, the time elapsed between the occurrence of an error caused by a bug and its manifestation as an observable failure. Symbolic QED combines QED principles with a formal engine for both pre- and post-silicon validation. Symbolic QED leverages incredible improvements in satisfiability solvers over the past decade, which we will also highlight in this tutorial. These techniques are effective for logic design bugs and electrical bugs inside processor cores, hardware accelerators, and uncore components (cache controllers, memory controllers, interconnection networks or power management units). Results from several commercial and open-source designs demonstrate:
1. For billion transistor-scale designs, one can now detect and localize difficult logic design bugs automatically in only a few (~3) hours during pre-silicon verification.
2. For open-source RISC-V processor cores, one can now uncover many real design bugs that were previously unknown within minutes automatically.
3. We will present an industry study on automotive designs (Infineon) –multiple iterations of custom automotive micro-controllers for several commercial automotive products. We will show how the presented methodology can enable designers to detect all the difficult bugs in the product quickly (in a few weeks, including setting up the methodology). In contrast, it took nearly a year or longer to detect these bugs using existing industrial verification methodologies.
4. One can now drastically improve error detection latencies of post-silicon validation tests by up to 9 orders of magnitude for quick debug, from billions of clock cycles to very few clock cycles, and simultaneously improve bug coverage.
5. One can now automatically localize bugs in billion-transistor-scale designs during post-silicon debug, e.g., one can narrow the location of an electrical bug to a handful of flip-flops (~18 for a design with ~1million flip-flops), in only a few (~9) hours.
In addition, attendees will participate in several hands-on activities:
1. Set up and run Symbolic QED for multiple open-source RISC-V processor cores and detect real logic bugs.
2. Set up and run Symbolic QED on a multi-core design, adapting Symbolic QED to a large design that cannot be analyzed by formal tools.
3. Set up and run Symbolic QED for open-source accelerators, and find real logic bugs.
4. QED post-silicon validation and debug (using an FPGA platform).