Regression testing is a technique to ensure that micro-electronic circuit design functionality is correct under iterative changes during the design process. This incurs significant costs in the hardware design and verification cycle in terms of productivity, machine and simulation software costs, and time - sometimes as much as 70% of the hardware design costs. We propose a machine learning approach to select a subset of tests from the set of all RTL regression tests for the design. Ideally, the selected subset should detect all failures that the full set of tests would have detected. Our approach learns characteristics of both RTL code and tests during the verification process to estimate the likelihood that a test will expose a bug introduced by an incremental design modification. This paper describes our approach to the problem and its implementation. We also present experiments on several real-world designs of various types with different types of test-suites that demonstrate significant time and resource savings while maintaining validation quality.

Methods based on machine learning (ML) are gaining increasing importance at various stages of the integrated circuit (IC) design flow including EDA applications. However, real-world EDA flows are constrained by dynamic changes in resource availability such as compute, license costs, and time-to-results in the IC-design life cycle. In addition, typical industrial ML models must deal with highly imbalanced datasets that pose challenges in maximizing model quality of results (QoR). This paper addresses the problem of optimizing ML model QoR in a resource-constrained environment. Our approach partitions the binary classification problem into that of first generating a high-quality calibrated discrete probability distribution over data and then poses the classification step as an optimization problem where the generated probabilities are used as dynamic weights in the constraint set. We propose a method to find close-to-optimal solutions to balance QOR with prediction latency and resource constraints. The proposed method is generic in that it applies to any binary classification problem that generates sets of predictions in the described environment of highly imbalanced data combined with user-defined QOR, prediction latency, and resource constraints. We present experimental results using our approach on an industrial ML model for verification regression test selection and compare it with default predictions to demonstrate the method’s effectiveness.

We present an efficient search strategy for satisfiability checking on circuits represented at the register-transfer-level (RTL). We use the RTL circuit structure by extending concepts from classic automatic test-pattern generation (ATPG) algorithms and interval-arithmetic to guide the search process. We extend the idea of Boolean recursive learning on predicate logic in the RTL using Boolean and interval constraint propagation in the control and data-path of the circuit. This is used as a pre-processing step to derive relations between predicate logic signals that are used to augment the search. We demonstrate experimentally that these methods provide significant improvement over current techniques on sample benchmarks.

We present new techniques for improving search in a hybrid Davis-Putnam-Logemann-Loveland based constraint solver for RTL (register-transfer level) circuits (HDPLL). In earlier work on HDPLL (Parthasarathy, G. et al., 41st DAC, 2004), the authors combined solvers for integer and Boolean domains using finite-domain constraint propagation with heuristic conflict-based learning. We describe a new algorithm that extends the conflict-based unique-implication point learning in Boolean SAT (satisfiability) solvers to hybrid Boolean-integer domains in HDPLL. We describe data-structures for efficient constraint propagation on the hybrid learned relations, similar to two-literal watching in Boolean SAT. We demonstrate that these new techniques provide considerable performance benefits when compared with other combinations of decision theories.

A sequential SAT solver, Satori, was recently proposed (Iyer, M.K. et al., Proc. IEEE/ACM Int. Conf. on Computer-Aided Design, 2003) as an alternative to combinational SAT in verification applications. This paper describes the design of Seq-SAT, an efficient sequential SAT solver with improved search strategies over Satori. The major improvements include: (1) a new and better heuristic for minimizing the set of assignments to state variables; (2) a new priority-based search strategy and a flexible sequential search framework which integrates different search strategies; (3) a decision variable selection heuristic more suitable for solving the sequential problems. We present experimental results to demonstrate that our sequential SAT solver can achieve orders-of-magnitude speedup over Satori. We plan to release the source code of Seq-SAT.

We present a method that combines interval-arithmetic (IA) and Boolean reasoning with structural hashing for simplifying SAT problems on circuits expressed at the register-transfer level. We demonstrate that simple transformations based on interval-arithmetic operations can significantly reduce the complexity of the problem. We identify cases where the inherent over-approximations in IA operations can be reduced. We demonstrate that these techniques can significantly reduce RTL-SAT instances in size and runtime.

We present a novel hybrid finite-domain constraint solving engine for RTL circuits, that automatically uses data-path abstraction. We describe how DPLL search can be modified by using efficient finite-domain constraint propagation to improve communication between interacting integer and Boolean domains. This enables efficient combination of Boolean SAT and linear integer arithmetic solving techniques. We use conflict-based learning using the variables on the boundary of control and data-path for additional performance benefits. Finally, the hybrid constraint solver is experimentally analyzed using some example circuits.

In the past, symbolic trajectory evaluation (STE) has been shown to be effective for verifying individual array blocks. However, when applying STE to verify multiple array blocks together as a single system, the run-time OBDD (ordered boolean decision diagrams) sizes would often blow up. In this paper, we propose the use of both an ATPG-based justification engine and symbolic simulation to facilitate the application of STE proof methodology for array systems. Our method translates a given verification problem instance into ATPG justification objectives, and partitions a given design into ATPG and symbolic simulation domains. Then, by developing a scheme that enables the ATPG justification engine to work closely with the symbolic simulator, the runtime OBDD sizes during each symbolic simulation run can be limited. We demonstrate the effectiveness of our approach by verifying the memory management units (MMU) in Motorola high-performance microprocessors. The verification of a MMU as a whole was not possible before because of the OBDD size blow-up problem when symbolic simulation is used in the STE proof process.

We utilize Rent's rule as an empirical measure for efficient clustering and placement of circuits in clustered Field Programmable Gate Arrays (FPGAs). We show that careful matching of resource availability and design complexity during the clustering and placement processes can contribute to spatial uniformity in the placed design, leading to overall device decongestion after routing. We present experimental results to show that appropriate logic depopulation during clustering can have a positive impact on the overall FPGA device area. Our clustering and placement techniques can improve the overall device routing area by as much as 62%, 35% on average, for the same array size, when compared to state-of-the-art FPGA clustering, placement, and routing tools. Power dissipation simulations using a typical buffered pass-transistor-based FPGA interconnect model are also presented. They show that our clustering and placement techniques can reduce the overall device power dissipation by approximately 13%.

Utilizes Rent's rule as an empirical measure for efficient clustering and placement of circuits on hierarchical FPGAs. We show that careful matching of design complexity and architecture resources of hierarchical FPGAs can have a positive impact on the overall device area. We propose a circuit placement algorithm based on Rent's parameter and show that our clustering and placement techniques can improve the overall device routing area by as much as 21% for the same array size, when compared to a state-of-art FPGA placement and routing tool.

We propose a novel hardware model to reconfigure a sequential ULSI circuit for partial-scanned delay-fault built-in self-test (BIST). We modify the standard stuck-fault BIST model to ensure highly robust delay tests by inserting hardware to avoid circuit hazards that invalidate delay tests. The model treats un-scanned flip-flops and latches as inverters or buffers. We propose a novel minimum feedback vertex set (FVS) algorithm based on quadratic 0-1 programming (which has O(n/sup 2/) complexity) for partial-scan flip-flop selection. We obtain a pipelined sequential circuit and insert parity-flippers to remove hazards during testing. We avoid placing hardware on time-critical paths. We find the FVS and insert deglitching hardware for all of the 1989 ISCAS circuits.