Clark Barrett

System-on-Chips (SoCs) are an integral part of our lives. The complexity of SoCs requires sophisticated tools and methods for ensuring functional correctness, especially in critical domains such as automotive and healthcare applications. In addition, the prevalence of security features in SoCs and emerging threats such as Spectre and Meltdown underscore the need for advanced verification techniques to combat security vulnerabilities. Existing verification approaches consume over 50% of development effort. Pre-silicon verification ensures functional correctness before chip fabrication, while post-silicon validation detects bugs that escape pre-silicon verification. Existing pre-silicon and post-silicon approaches are inadequate resulting in skyrocketing bug escapes and respins. To address these challenges, this book presents pre-silicon verification and post-silicon validation methods based on Quick Error Detection (QED) principles: self-consistency checking to detect and localize design bugs. Symbolic QED combines QED principles with model checking (a formal verification technique) for pre-silicon verification. Many studies, including industrial case studies, have demonstrated the effectiveness and practicality of Symbolic QED. QED-based methods for post-silicon validation significantly reduce the error detection latency (the time elapsed between the occurrence of a bug and its manifestation as an observable failure) by several orders of magnitude, addressing the limitations of existing validation and debug approaches. This book also discusses Unique Program Execution Checking (UPEC), a hardware security verification technique inspired by QED principles. Beyond the specific QED techniques described here, a new pre-silicon verification approach called G-QED (Generalized Quick Error Detection) is already demonstrating significant drastic benefits for pre-silicon verification of a wide variety of designs.

Every major technical invention resurfaces the dual-use dilemma -- the new technology has the potential to be used for good as well as for harm. Generative AI (GenAI) techniques, such as large language models (LLMs) and diffusion models, have shown remarkable capabilities (e.g., in-context learning, code-completion, and text-to-image generation and editing). However, GenAI can be used just as well by attackers to generate new attacks and increase the velocity and efficacy of existing attacks.This monograph reports the findings of a workshop held at Google (co-organized by Stanford University and the University of Wisconsin-Madison) on the dual-use dilemma posed by GenAI. This work is not meant to be comprehensive, but is rather an attempt to synthesize some of the interesting findings from the workshop. Short-term and long-term goals for the community on this topic are discussed. This work should provide both a launching point for a discussion on this important topic, as well as interesting problems that the research community can work to address.

Neural networks have been widely used in many applications, such as image classification and understanding, language processing, and control of autonomous systems. These networks work by mapping inputs to outputs through a sequence of layers. At each layer, the input to that layer undergoes an affine transformation followed by a simple nonlinear transformation before being passed to the next layer. Neural networks are being used for increasingly important tasks, and in some cases, incorrect outputs can lead to costly consequences, hence validation of correctness at each layer is vital. The sheer size of the networks makes this not feasible using traditional methods. In this monograph, the authors survey a class of methods that are capable of formally verifying properties of deep neural networks. In doing so, they introduce a unified mathematical framework for verifying neural networks, classify existing methods under this framework, provide pedagogical implementations of existing methods, and compare those methods on a set of benchmark problems. Algorithms for Verifying Deep Neural Networks serves as a tutorial for students and professionals interested in this emerging field as well as a benchmark to facilitate the design of new verification algorithms.