Proof decomposition via assume-guarantee with helper properties, i.e. helpers, is one of the most promising approaches to address the complexity of hardware formal verification (FV). While helpers can be hand-crafted by human experts, state-of-the-art methods replace this labor-intensive process with circuit analysis, from which a large set of helper candidates can be quickly synthesized. However, these candidates are often of lower-quality, and distilling the full auto-generated set down to a subset of high-quality, appropriate helpers still requires significant computational or manual effort. In this work, we propose a novel approach to automate helper quality assessment: Learned Formal Proof Strengthening (LFPS), a neural model that can accurately predict helper effectiveness without having to run actual formal proofs. The LFPS model jointly learns representations of property specifications expressed in SystemVerilog and the graph representation of the circuit under verification. When evaluated against three RTL designs from industrial SoCs, our model is shown to achieve significant predictive performance, with an average of 98.2% accuracy and 98.3% F-1 score. Once trained, the model can also serve as a fast predictor for search algorithms: we show that LFPS neural-guided search can outperform random sampling in finding sets of helper candidates that achieve inductive proof strengthening.

We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking -- however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

The required manual effort and verification expertise are among the main hurdles for adopting formal verification in processor design flows. Developing a set of properties that fully covers all instruction behaviors is a laborious and challenging task. This paper proposes a highly automated and "complete" processor verification approach which requires considerably less manual effort and expertise compared to the state of the art.The proposed approach extends the S2QED approach to cover both single and multiple instruction bugs and ensures that a design is completely verified according to a well-defined criterion. This makes the approach robust against human errors. The properties are simple and can be automatically generated from an ISA model with small manual effort. Furthermore, unlike in conventional property checking, the verification engineer does not need to explicitly specify the processor's behavior in different special scenarios, such as stalling, exception, or speculation, since these scenarios are taken care of implicitly by the proposed computational model. The great promise of the approach is shown by an industrial case study with a 5-stage RISC-V processor.

We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several microcontroller core designs (~1,800 flip-flops, ~70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. (These additional bugs were also perhaps detected by the industrial verification flow.)3.Symbolic QED enables significant design productivity improvements: (a) 8X improved (i.e., reduced) verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED.

As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic and security bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.

During post-silicon validation and debug, manufactured integrated circuits (ICs) are tested in actual system environments to detect and fix design flaws (bugs). Existing post-silicon validation and debug techniques are mostly ad hoc and often involve manual steps. Such ad hoc approaches cannot scale with increasing IC complexity. We present Symbolic Quick Error Detection (Symbolic QED), a structured approach to post-silicon validation and debug. Symbolic QED combines the following steps in a coordinated fashion: 1. Quick Error Detection (QED) tests that quickly detect bugs with short error detection latencies and high coverage. 2. Formal analysis techniques to localize bugs and generate minimal-length bug traces upon detection of the corresponding bugs. We demonstrate the practicality and effectiveness of Symbolic QED using the OpenSPARC T2, a 500-million-transistor open-source multicore System-on-Chip (SoC) design, and using "difficult" logic bug scenarios that occurred in various state-of-the-art commercial multicore SoCs. Our results show that Symbolic QED: (i) is fully automatic (unlike manual techniques in use today that can be extremely time-consuming and expensive); (ii) requires only a few hours in contrast to manual approaches that might take days (or even months) or formal techniques that often take days or fail completely for large designs; (iii) generates counter-examples (for activating and detecting logic bugs) that are up to 6 orders of magnitude shorter than those produced by traditional techniques; and, (iv) does not require any additional hardware.

3D-Stacked ICs manufactured from wafer to wafer stacking are known to suffer from significant yield degradation from the compounding of the defect probabilities for individual dies. However, recent experiments, based on carefully simulated wafer defect maps and validated by silicon data, have shown that traditional yield estimates for 3D-SICs that assume uniform defect probabilities across the stacked wafers can be pessimistic by up to 50%. This is due to yield variations at the different die locations on the wafer resulting from the commonly observed clustering of defects, and also from systematic defects introduced by equipment and handling issues during manufacturing. In this paper we present a novel 3D-SIC yield model which for the first time accurately estimates the impact of this location based wafer die yield variation on the 3D-SIC yield. We further develop a simplified compact model that uses the average die yield, and two easy to obtain parameters (a and σ) that capture the essential spatial information needed for accurately estimating the 3D-SIC yields. The new models are extensively validated against both simulated defect maps and actual silicon data. They promise to greatly simplify meaningful study of cost trade-offs while exploring implementation options for 3D-SICs early in the design phase.

We present and evaluate a simulation methodology to model the impact of the radial clustering of defects on wafers on the yield of 3D ICs manufactured using wafer to wafer stacking. Our simulations draw on an extensively validated model for radial yield degradation on wafers from the literature to incorporate the effect of this key contributor to the widely observed clustering of defects on semiconductor wafers. Current 3D-SIC yield estimation methods ignore defect clustering and assume a uniform distribution of defective dies on each wafer. Our results show that the radial clustering of defective dies causes stacked die yields to be significantly higher than that projected by current models. For 4-5 layer stacks the difference can be 50% or more. Our simulation studies are further validated by comparison with actual silicon data, which suggests that even the more accurate yield estimates from our improved methodology may be somewhat pessimistic. Thus the results presented here show that in practice degradation in stacked die yield from compounding may not be as severe as commonly estimated. This has significant implications in evaluating cost trade-offs associated with 3D-SIC manufacturing.

Three-dimensional Stacked Integrated Circuit packages interconnected using high speed Through-Silicon Via technology can be efficiently manufactured using a wafer-to-wafer stacking process. Efforts to mitigate degradation in the composite yield of the stacked die are primarily focused on matching defect maps while assigning the pre-tested wafers from the available wafer repository to individual wafer stacks. In this paper we show how rotational symmetry can be exploited to increase the number of available wafer defect maps by a factor of four, thereby significantly improving matching possibilities and hence yield. We further apply our approach to processor-memory stacks, with relatively high memory die yield from redundancy and repair, for which we also present new heuristic matching algorithms. Altogether, our new approach shows viable absolute yields, with yield improvement of better than 25% over stacking without any matching. This is a significant advance over earlier results.