Given a design variable and its fanin cone, determining whether one fanin variable has controlling power over other fanin variables can benefit many design steps such as verification, synthesis and test generation. In this work we formulate this path controllability problem and propose several algorithms that not only solve this problem but also return values that enable or block other fanin variables. Empirical results show that our algorithms can effectively perform path controllability analysis and help produce high-quality designs.

Retention registers are utilized in power gating design to hold design state during power down and to allow safe and fast system reactivation. Since a retention register consumes more power and costs more area than a non-retention register, it is desirable to minimize the use of retention registers. However, relaxing retention requirement to a minimal subset of registers can be computationally challenging. In this paper, we adopt satisfiability solving for scalable selection of registers whose retention is unnecessary and exploit input sequence constraints to increase the number of non-retention registers. Empirical results on industrial benchmarks show that our proposed methods are efficient and effective in identifying non-retention registers.

Unknown values (Xs) may exist in a design due to uninitialized registers or blocks that are powered down. Due to X-pessimism in gate-level logic simulation, such Xs cannot be handled correctly, producing false Xs that result in inaccurate simulation values. To improve gate-level simulation accuracy when Xs exist, we first trace the fan-in cone of Xs to check whether they are real. For the Xs that are not real, we extract small sub-circuits responsible for creating the false Xs. We then generate auxiliary code to repair gate-level simulation by replacing the Xs with the correct values. Our experimental results on commercial designs show that the proposed methods are both effective and efficient.

At-speed testing is increasingly important at recent technology nodes due to growing uncertainty in chip manufacturing. However, at-speed fault coverage and test-efficacy suffer when tests are not robust. Since Automatic Test Pattern Generation (ATPG) is typically performed at late design stages, fixing robustness problems found during ATPG can be costly. To address this challenge, we propose a methodology that identifies robustness problems at the Register Transfer Level (RTL) and fixes them. Empirically, this improves final at-speed fault coverage and test-efficacy.

Achieving high coverage is an important goal in design verification. Fixing coverability problems found at the verification stage, however, can require tremendous effort. To address this problem, we propose a flow for analyzing code and variable-toggle coverability at the early-RTL block-level stage. In addition, we devise a novel technique to analyze the coverability problems so that engineers can resolve the issues more efficiently. By identifying coverability problems at early RTL design stages, design verifiability can be improved, thus reducing the effort required at the verification phase.

Code coverage is a popular method to find design bugs and verification loopholes. However, once a piece of code is determined to be unreachable, diagnosing the cause of the problem can be challenging: since the code is unreachable, no counterexample can be returned for debugging. Therefore, engineers need to analyze the legality of nonexistent execution paths, which can be difficult. To address such a problem, we analyzed the cause of unreachability in several industrial designs and proposed a diagnosis technique that can explain the cause of unreachability. In addition, our method provides suggestions on how to solve the un-reachability problem, which can further facilitate debugging. Our experimental results show that this technique can greatly reduce an engineer's effort in analyzing unreachable code.

Reset is one of the most important signals in many designs. Since reset is typically not timing critical, it is handled at late physical design stages. However, the large fanout of reset and the lack of routing resources at these stages can create variant delays on different targets of the reset signal, creating reset recovery problems. Traditional approaches address this problem using physical design methods such as buffer insertion or rerouting. However, these methods may invalidate previous optimization efforts, making timing closure difficult. In this work we propose a formal method to calculate reset recovery slacks for registers at the register transfer level. Designers and physical design tools can then utilize this information throughout the design flow to reduce reset problems at later design stages.

Most synthesis tools perform optimizations based on the design itself and do not utilize the information present in the verification environment. Not using such information greatly limits the optimization capabilities of synthesis tools, which is especially serious for circuit customization because most environment constraints are encoded in the testbench. To exploit verification intention, we propose a methodology that utilizes functional assertions for design optimization. To support circuit customization, we also propose a property mining technique that can extract properties from the design under the constraints in the testbench. Our experimental results show that these methods can reduce design size after synthesis, and the optimization is orthogonal to other existing circuit customization methods.

Optimizing blocks in a System-on-Chip (SoC) circuit is becoming more and more important nowadays due to the use of third-party Intellectual Properties (IPs) and reused design blocks. In this paper, we propose techniques and methodologies that utilize abundant external don't-cares that exist in an SoC environment for block optimization. Our symbolic code-statement reachability analysis can extract don't-care conditions from constrained-random testbenches or other design blocks to identify unreachable conditional blocks in the design code. Those blocks can then be removed before logic synthesis is performed to produce smaller and more power-efficient final circuits. Our results show that we can optimize designs under different constraints and provide additional flexibility for SoC design flows.

Due to increases in design complexity, routing a reset signal to all registers is becoming more difficult. One way to solve this problem is to reset only certain registers and rely on a software initialization sequence to reset other registers. This approach, however, may allow unknown values (also called X-values) in uninitialized registers to leak to other registers, leaving the design in a nondeterministic state. Although logic simulation can find some X-problems, it is not accurate and may miss bugs. A recent approach based on symbolic simulation can handle Xs accurately; however, it is not scalable. In this work we analyze the characteristics of X-problems and propose a methodology that leverages the accuracy of formal X-analysis and can scale to large designs. This is achieved by our novel partitioning techniques and the intelligent use of waveforms as stimulus. We applied our methodology to an industrial design and successfully identified several Xs unknown to the designers, including three real bugs, demonstrating the effectiveness of our approach.

Don't-care conditions are utilized by many synthesis tools because such conditions provide additional flexibility for logic optimization. However, most techniques only focus on the gate level because it is difficult to handle such conditions accurately at behavior and register transfer levels. This is problematic since the trend is to move toward high-level synthesis. In this paper, we propose innovative methods to handle such conditions accurately at high-level designs. In addition, we propose three novel algorithms based on our new methods to minimize the number of registers that need to be initialized, which can reduce the routing resources used by the reset signals and alleviate the routing problem. We applied our techniques to a five-stage pipelined processor and successfully reduced the number of control registers that need to be initialized by 53%, demonstrating the effectiveness of our approach.

Traditional digital circuit synthesis flows start from an HDL behavioral definition and assume that circuit functions are almost completely defined, making don't-care conditions rare. However, recent design methodologies do not always satisfy these assumptions. For instance, third-party IP blocks used in a system-on-chip are often overdesigned for the requirements at hand. By focusing only on the input combinations occurring in a specific application, one could resynthesize the system to greatly reduce its area and power consumption. Therefore we extend modern digital synthesis with a novel technique, called SWEDE, that makes use of extensive external don't-cares. In addition, we utilize such don't-cares present implicitly in existing simulation-based verification environments for circuit customization. Experiments indicate that SWEDE scales to large ICs with half-million input vectors and handles practical cases well.

Don't-care conditions provide additional flexibility in logic synthesis and optimization. However, most work only focuses on the gate level because it is difficult to handle such conditions accurately at the behavior and register transfer levels, which is problematic since the trend is to move toward high-level synthesis. In this work we propose innovative methods to handle such conditions accurately at high-level designs. In addition, we propose two novel algorithms based on our new methods to minimize the number of registers that need to be initialized at the architecture level, which can reduce the routing resources used by the reset signals and alleviate the routing problem. Our results show that we can identify 53% of the registers that can be uninitialized in a 5-stage pipelined processor within 5 minutes, demonstrating the effectiveness of our approach.

Traditional digital circuit synthesis flows start from an HDL behavioral definition and assume that circuit functions are almost completely defined, making don't-care conditions rare. However, recent design methodologies do not always satisfy these assumptions. For instance, third-party IP blocks used in a system-on-chip are often over-designed for the requirements at hand. By focusing only on the input combinations occurring in a specific application, one could resynthesize the system to reduce its area and power consumption. Therefore we extend modern digital synthesis with a novel technique, called SWEDE, that uses external don't-cares present implicitly in existing simulation-based verification environments for circuit customization. Experiments indicate that SWEDE scales to large ICs with half-million input vectors and handles practical cases well.

The miniaturization of transistors in recent technology nodes requires tremendous back-end tuning and optimizations, making bug fixing at later design stages more expensive. Therefore, it is imperative to find design bugs as early as possible. The first defense against bugs is block-level testing performed by designers, and constrained-random simulation is the prevalent method. However, this method may miss corner-case scenarios. In this paper we propose an innovative methodology that reuses existing constrained-random testbenches for formal bug hunting. To support the methodology, we present several techniques to enhance RTL symbolic simulation, and integrate state-of-the-art word-level and Boolean-level verification techniques into a common framework called BugHunter. From case studies DLX, Alpha and FIR, BugHunter found more bugs than constrained-random simulation using fewer cycles, including four new bugs in the verified design previously unknown to the designer. The results demonstrate that the proposed techniques provide a flexible, scalable and robust solution for bug hunting.

Post-silicon validation has recently become a major bottleneck in IC design. Several high profile IC designs have been taped-out with latent bugs, and forced the manufacturers to resort to additional design revisions. Such changes can be applied through metal fix; however, this is impractical without carefully pre-placed spare cells. In this work we perform the first comprehensive analysis of the issues related to spare-cell insertion, including the types of spare cells that should be used as well as their placement. In addition, we propose a new technique to measure the heterogeneity among signals and use it to determine spare-cell density. Finally, we integrate our findings into a novel multi-faceted approach that calculates regional demand for spare cells, identifies the most appropriate cell types, and places such cells into the layout. Our approach enables the use of metal fix at a much smaller delay cost, with a reduction of up to 37% compared to previous solutions

In this paper, we propose a resynthesis framework, called COunterexample-guided REsynthesis (CoRe), that automatically corrects errors in digital designs. The framework is based on a simulation-based abstraction technique and performs an error correction through two innovative circuit resynthesis solutions: distinguishing-power search and goal-directed search, which modify the functionality of circuits' internal nodes to match the correct behavior. In addition, we propose a compact encoding of resynthesis information, called the Pairs of Bits to be Distinguished, which is a key enabler for our resynthesis techniques. Compared with previous solutions, CoRe is more powerful for the following reasons: (1) It can fix a broader range of error types because it is not bounded by specific error models; (2) it derives the correct functionality from simulation vectors without requiring golden netlists; and (3) it can be applied with a broad range of verification flows, including formal and simulation-based flows.

Physical synthesis is a relatively young field in electronic design automation. Many published optimizations for physical synthesis end up hurting the final result, often by neglecting important physical aspects of the layout, such as long wires or routing congestion. In this work we propose SafeResynth, a safe resynthesis technique, which provides immediately-measurable delay improvement without altering the design's functionality. It can enhance circuit timing without detrimental effects on route length and congestion. When applied to IWLS'05 benchmarks, SafeResynth improves circuit delay by 11% on average after routing, while increasing route length and via count by less than 0.2%. Our resynthesis can also be used in an unsafe mode, akin to more traditional physical synthesis algorithms popular in commercial tools. Applied together, our safe and unsafe transformations achieve 24% average delay improvement for seven large benchmarks from the OpenCores suite. The relative contribution of safe and unsafe techniques varies depending on the amount of whitespace in the layout.

In this work we propose a new error-correction framework, called CoRe, which uses counterexamples, or bug traces, generated in verification to automatically correct errors in digital designs. CoRe is powered by two innovative resynthesis techniques, goal-directed search (GDS) and entropy-guided search (EGS), which modify the functionality of internal circuit's nodes to match the desired specification. We evaluate our solution to designs and errors arising during combinational equivalence-checking, as well as simulation-based verification of digital systems. Compared with previously proposed techniques, CoRe is more powerful in that: (1) it can fix a broader range of error types because it does not rely on specific error models; (2) it derives the correct functionality from simulation vectors, hence not requiring golden netlists; and (3) it can be applied to a range of verification flows, including formal and simulation-based.

SAT sweeping is the process of merging two or more functionally equivalent nodes in a circuit by selecting one of them to represent all the other equivalent nodes. This provides significant advantages in synthesis by reducing circuit size and provides additional flexibility in technology mapping, which could be crucial in post-synthesis optimizations. Furthermore, it is also critical in verification because it can reduce the complexity of the netlist to be analyzed in equivalence checking. Most algorithms available so far for this goal do not exploit observability don't cares (ODCs) for node merging since nodes equivalent up to ODCs do not form an equivalence relation. Although a few recently proposed solutions can exploit ODCs by overcoming this limitation, they constrain their analysis to just a few levels of surrounding logic to avoid prohibitive runtime. We develop an ODC-based node merging algorithm that performs efficient global ODC analysis (considering the entire netlist) through simulation and SAT. Our contributions which enable global ODC-based optimizations are: (1) a fast ODC-aware simulator and (2) an incremental verification strategy that limits computational complexity. In addition, our technique operates on arbitrarily mapped netlists, allowing for powerful post-synthesis optimizations. We show that global ODC analysis discovers on average 25% more (and up to 60%) node-merging opportunities than current state-of-the-art solutions based on local ODC analysis.

Modern IC designs have reached unparalleled levels of complexity, resulting in more and more bugs discovered after design tape-out However, so far only very few EDA tools for post-silicon debugging have been reported in the literature. In this work we develop a methodology and new algorithms to automate this debugging process. Key innovations in our technique include support for the physical constraints specific to post-silicon debugging and the ability to repair functional errors through subtle modifications of an existing layout. In addition, our proposed post-silicon debugging methodology (FogClear) can repair some electrical errors while preserving functional correctness. Thus, by automating this traditionally manual debugging process, our contributions promise to reduce engineers’ debugging effort. As our empirical results show, we can automatically repair more than 70% of our benchmark designs.

Finding the cause of a bug can be one of the most time-consuming activities in design verification. This is particularly true in the case of bugs discovered in the context of a random-simulation-based methodology, where bug traces, or counterexamples, may be several hundred thousand cycles long. In this paper, BUg TRAce MINimization (Butramin), which is a bug trace minimizer, is proposed. Butramin considers a bug trace produced by a random simulator or semiformal verification software and produces an equivalent trace of shorter length. Butramin applies a range of minimization techniques, deploying both simulation-based and formal methods, with the objective of producing highly reduced traces that still expose the original bug. Butramin was evaluated on a range of designs, including the publicly available picoJava microprocessor, and bug traces up to one million cycles long. Experiments show that in most cases, Butramin is able to reduce traces to a very small fraction of their initial sizes, in terms of cycle length and signals involved. The minimized traces can greatly facilitate bug analysis and reduce regression runtime

We propose two new algorithms for rewiring: a postplacement optimization that reconnects pins of a given netlist without changing the logic function and gate locations. In the first algorithm, we extract small subcircuits consisting of several gates from the design and reconnect pins according to the symmetries of the subcircuits. To enhance the power of symmetry detection, we also propose a graph-based symmetry detector that can identify permutational and phase-shift symmetries on multiple input and output wires, as well as hybrid symmetries, creating abundant opportunities for rewiring. Our second algorithm, called long-range rewiring, is based on reconnecting equivalent pins and can augment the first approach for further optimization. We apply our techniques for wirelength optimization and observe that they provide wirelength reduction comparable to that achieved by detailed placement.

Finding the cause of a bug can be one of the most time-consuming activities in design verification. This is particularly true in the case of bugs discovered in the context of a random simulation- based methodology, where bug traces, or counter-examples, may contain several hundred thousand cycles. In this work we propose Butramin, a bug trace minimizer. Butramin considers a bug trace produced by a random simulator or a semi-formal verification software and produces an equivalent trace of shorter length. Butramin applies a range of minimization techniques, deploying both simulation-based and formal methods, with the objective of producing highly reduced traces that still expose the original bug. We evaluated Butramin on a range of designs, including the publicly available picoJava microprocessor. Our experiments show that in most cases Butramin is able to reduce traces to a small fraction of their initial size, in terms of cycle length and signals involved.

Separate optimizations of logic and layout have been thoroughly studied in the past and are well documented for common benchmarks. However, to be competitive, modern circuit optimizations must use physical and logic information simultaneously. In this work, we propose new algorithms for rewiring and rebuffering - a post-placement optimization that reconnects pins of a given netlist without changing the logic function and gate locations. These techniques are compatible with separate layout and logic optimizations, and appear independent of them. In particular, when the new optimization is applied before or after detailed placement, it approximately doubles the improvement in wirelength. Our contributions are based on exhaustive search for functional symmetries in sub-circuits consisting of several gates. Our graph-based symmetry finding is more comprehensive than previously known algorithms - it detects permutational and phase-shift symmetries on multiple input and output wires, as well as hybrid symmetries, creating more opportunities for rewiring and rebuffering.