G-QED Pre-silicon Verification

Speaker: Saranyu Chattopadhyay, PhD Student, Stanford University
Date: June 14, 2023

G-QED -- Generalized Quick Error Detection -- is a highly thorough pre-silicon verification technique that significantly boosts design productivity. G-QED can be applied to any digital design that satisfies the following conditions: (1) actions, architectural states and idling, similar to instructions, software-visible states and idling in processors, can be defined; and, (2) the content of each architectural state element can be read by an action to produce corresponding design outputs. G-QED is provably sound and complete, i.e., it detects all logic bugs without any false fails, within the capabilities of existing Bounded Model Checking (BMC) tools. Results on a wide range of processor and hardware accelerator designs demonstrate the effectiveness and practicality of G-QED. For an industrial case study using production-ready AI engines, G-QED detected 9 new critical bugs (in addition to all bugs detected by the industrial verification flow) with a drastic productivity boost -- 3 person weeks of verification effort using G-QED vs. 1 person-year using the industrial verification flow. If time permits, we will also discuss possible ways to scale up G-QED for very large designs that existing BMC tools cannot handle.