Engineering Change Order (ECO) and logic debugging problems where multiple locations in the circuit must be modified are formulated with Quantified Boolean Function (QBF) and set-sovering techniques. The formulation is based on the fanin selection method for each gate. Although the resulting formulation for single portion changes is basically equivalent to Sets of Pairs of Functions to be Distinguished (SPFD) [3], the way of its computations is quite different. Moreover, the simultaneous changes for multipl portions becomes Boolean Relation extension of SPFD. Experimental results and applications to various logic optimization problems are also shown.

As the number of transistors in the fabricated circuits becomes extremely larger, not only single stuck-at faults, but also multiple stuck-at faults (MSAFs) are likely to happen in the circuits, especially for the large-scale circuit. Multiple faults are difficult to be fully covered due to the exponentially enormous number of all possible faults. Although there are methods proposed to deal with the multiple faults, they fail to generate compact test patterns to detect all faults within an acceptable running time. In order to solve these problems, this article proposes an incremental automatic test pattern generation method to deal with MSAFs. Instead of traversing the entire n multiple fault list, the proposed method only selects the faults undetected by the existing test patterns for n - 1 faults, and then generates additional test patterns. Staring from a complete test set for single faults, the proposed ATPG method can be incrementally applied to handle all multiple faults. Moreover, since the number of undetected faults that are selected is extremely smaller comparing to the total number of the entire fault list, the proposed method can generate compact test patterns to cover all faults within an acceptable running time.

This paper proposes methods to get a minimally rectified logic circuit equivalent to a new specification. One of the proposed methods can deal with multiple target signals to be modified at the same time. Moreover, a graph-cut based method is proposed to reduce the search space. In the case the problem is difficult to be handled by the at-the-same-time method, an enhanced method is proposed to efficiently deal with the target signals one by one. The quality of results on ICCAD'17 contest benchmarks is equally good or better, average 16 times better score, than the previous work.

Mapping of large systems/computations on multiple chips/multiple cores needs sophisticated compilation methods. In this demonstration, we present our compiler tools for multi-chip and multi-core systems that considers communication architecture and the related constraints for optimal mapping. Specifically, we demonstrate compilation methods for multi-chip connected with ring topology, and multi-core connected with mesh topology, assuming fine-grained reconfigurable cores, as well as generalization techniques for large problems size as convolutional neural networks. We will demonstrate our mappings methods starting from data-flow graphs (DFGs) and equations, specifically with applications to convolutional neural networks (CNNs) for convolution layers as well as fully connected layers.

In this paper, we present a technique to automatically adjust Register-transfer level (RTL) implementation for Engineering Change Order (ECO) in high level. Our method focuses on the datapath structure, where circuit topologies are mostly, and only partial portions are replaced by programmable datapath. Exploring the correct configuration of the datapath is formulated as Quantified Boolean Formula (QBF) problem, and can be solved by using Satisfiability (SAT) /Satisfiability Modulo Theories (SMT) solver in an incremental way automatically. The experimental results with several example cases have confirmed that effectiveness of the proposed method.

Approximate computing can be applied to error-tolerant applications, by trading off accuracy for lower power consumption, shorter delay and smaller area. In this paper, we focus on the approximate arithmetic circuit design especially targeting combinational multipliers and adders, which are essential computing components in machine learning such as neural network computation. We propose a novel approach to generate approximate circuits from the given correct circuits. The basic idea is to study the circuit's characteristics from the small instances of the circuits and then establish a common algorithm for larger circuits with the same architectures. We propose two different methods and apply them to adders and multipliers with different architectures. The experimental results demonstrate that our method outperforms the state-of-art methods in terms of the quality of the circuits with orders of magnitude shorter processing time.

This paper proposes an incremental ATPG method to deal with multiple stuck-at faults. In order to generate the test set for n multiple faults, only the additional test patterns for the undetected faults by the existing test patterns for n - 1 multiple faults are generated. Moreover, by introducing an efficient fault selection method, the size of the fault list to be dealt with is reduced drastically compared to the entire fault list of n multiple faults. Our experimental results on ISCAS 89 and IWLS 2005 benchmarks up to triple faults indicate that the proposed method can generate a compact test set to cover all the faults within an acceptable runtime.

Post-silicon debug is the task of finding the bugs that could not be found before manufacturing. Electrical bugs are an important category of post-silicon bugs that are typically hard to debug due to complex interdependence of layout and netlist as well as their dependency to the running workload and environment. In this paper, we tackle the problem of debugging electrical bugs using trace buffers. Given an erroneous values captured in the trace buffer due to occurrence of an electrical bug, we try to identify the spatial and temporal location of the error. We have formulated the problem of debugging electrical bugs as a SAT problem and proposed a debugging method based on that. Moreover, we have shown that the existing signal selection methods for logical bugs that are typically trying to maximize signal restoration ratio (SRR) metric, do not perform better than random selection when debugging electrical bugs. On the other hands, utilizing a more sophisticated signal selection that is considering propagation of bit-flips due to electrical bugs is more effective.

As fabricated chips get larger and denser, more kinds of defects happen that cannot be explained by the traditional stuck-at-fault model. In this paper, we propose a new approach for diagnosis of bridging faults based on analysis of the logic design. The proposed approach is based on iteratively solving SAT problems until finding the internal signals that can explain the misbehavior of the circuit caused by bridging faults. Our experiments on ISCAS circuits shows efficiency and effectiveness of our method.

Previous works have shown that given an initial set of test patterns for single faults, relatively few additional tests are required to cover all multiple faults. In this paper, the exact situations in which the test patterns for single stuck-at faults do not detect multiple stuck-at faults are examined. We present proofs which show the conditions that is required to be met for ATPG on single faults to cover all multiple faults. Based on this analysis, we propose a new incremental ATPG method which first targets only single faults and then incrementally expands it to multiple faults with larger cardinalities, and present the experimental results for double faults.

This paper presents an area-efficient approximate method for 32-point transform which is one of the most area-consuming parts in High Efficiency Video Coding (HEVC) applications. Compared to prior literatures, this work reduces the hardware cost of transform by 1) eliminating all the arithmetic operations of 6 least significant bits (LSB), 2) presenting a low-delay method for generating carry propagation from the remaining 5 LSBs and 3) truncating the most significant bits (MSB) according to the position of component. In the implementation of a 32-point forward transform, the experimental results show that 27% area consumption can be saved and the coding efficiency loss aroused by the approximation is only 0.044% compared with the origin.

Engineering change orders (ECO) are small changes in the design due to last minute bug fixes or spec changes. In this paper, we focus on functional ECO in a logic design and try to construct the new logic function, reusing the existing logic as much as possible. Traditional approaches try to find appropriate locations in the original design that their modifications may result in the new functionality. However, those methods usually fail if additional inputs are required. We propose a new approach based on iterative SAT solving to find the inputs of the function for the given internal nodes, or the primary outputs that are the target of the ECO, out of all the internal signals and primary inputs such that it is guaranteed to be able to correct the functionality without explicitly generating the functions. Our experimental results on ITC99 benchmarks show the efficiency and effectiveness of our approach, specially for hard ECO cases.

Traditional debugging methods try to find an appropriate function of the given inputs for the internal nodes such that the modified circuit becomes correct. In this paper, we propose a new approach based on iterative SAT solving to find the inputs of the function for the internal nodes out of all the internal signals and primary inputs such that it is guaranteed to be able to correct the functionality without explicitly generating the functions. Our experimental results on ITC'99 benchmarks shows the efficiency and effectiveness of our approach.

In post-silicon debugging, only a limited number of states (flip-flops) can be traced, due to the area overhead that is introduced by trace buffers. Therefore, it is important to select the states which can restore most of the other states. There exist researches that try to heuristically select a set of flip-flops (FFs) which maximizes the number of restored FFs. We first show that those existing works are not so robust, as the cost functions used for selections do not work well in some cases. In this paper, we introduce a new signal selection that tries to improve the selection by swapping the FFs that are going to be traced. Furthermore, we introduce a hardware implementation of the method that is more than 3 orders of magnitude faster than software-based swapping. With the proposed methods, we can improve the signal selection and get consistent results even for large circuits.

We introduce a new approach for circuit matching using signatures. We have introduced a signature based on the topology of the fanin cone of each circuit element. First, we generate the signature for each circuit element. Then, we find all the circuit elements with unique signature among the given circuits. Finally, we expand the matching area by our expansion rules. Our experiments on IWLS2005 benchmark suite show that our method is able to find the perfect matching between two 160,000-gate IP in 43 minutes. In addition, our method is more than one order of magnitude faster than a state of the art graph matching based approach, while the size of the matched area is more than 30% larger.

We propose a method for rectification of bugs in microprocessors that are implemented on FPGAs, by only changing the configuration of LUTs, without any modification to the routing. Therefore, correcting the bugs does not require resynthesis, which can be very long for complex microprocessors due to possible timing closure problems. As the structure of the circuit is preserved, correcting the bugs does not affect the timings of the circuit. In design phase, we may add additional LUTs to the original circuit, so that we can use them in the correction phase. After a bug is found, we perform the following two tasks. Fist, we find the candidate control signals as well as the required change to correct their behavior. This is done by using symbolic simulation and equivalency checking between the formal specification and the erroneous formal model of the processor. Then, we try to map the corrected functionality into the existing LUT structure. This is done by a novel method that formulates the problem as a QBF (Quantified Boolean Formula) problem, and solves it by repeatedly applying normal SAT solvers instead of QBF solvers under a CEGAR (Counter Example Guided Abstraction Refinement) paradigm. We show effectiveness of our method by correcting bugs in two complex out-of-order superscalar processors with two different timing error recovery mechanisms.

In this paper, we propose an automated method for debugging and rectification of logical bugs in processors that are implemented on FPGAs. Our method is based on preserving the current circuit topology, and debugging and rectifying bugs by only changing the contents of LUTs, without any modification to the wiring. As a result, correcting the bugs does not require re-synthesis, which can be very time consuming for complex processors due to possible timing closure problems. As the topology of the circuit is preserved, correcting the bugs does not affect the timings of the circuit. In the design phase, we may add additional LUTs or additional inputs to LUTs in the original circuit, so that we can use them in debugging and rectification phase. After a bug is found, first we try to identify the candidate signals as well as their required changes to correct their behavior. This is achieved by using symbolic simulation and equivalence checking between an instruction-set architecture model of the processor and its erroneous model at micro-architecture level. Then, we try to map the corrected functionality into the existing LUT topology. This is realized by a novel method that formulates the problem as a QBF (Quantified Boolean Formula) problem, and solves it by repeatedly applying normal SAT solvers incrementally instead of QBF solvers utilizing ideas from CEGAR (Counter Example Guided Abstraction Refinement) paradigm. We show effectiveness as well as efficiency of our method by correcting bugs in two complex out-of-order superscalar processors with a timing error recovery mechanism.

This paper presents a method for automatic diagnosis and correction of design bugs in processors. Given a golden sequential instruction-set architecture model of a processor and its erroneous detailed cycle-accurate model at micro-architecture level, we employ a symbolic simulator and a property checker in an iterative process to formally find the candidate buggy locations and their corresponding fixes, without requiring an error model. We have shown the effectiveness of our method on a complex out-of-order super scalar processors supporting atomic execution.

In this paper, we address the problem of automatic correction of design errors in microprocessors, when the correction function is implemented in lookup tables. The formal specification of an erroneous processor and its reference instruction-set architecture (ISA) model are used in an iterative process, employing formal methods, to find and fix the bugs. Then, the correction function is optimized to reduce the lookup table size. We have shown the effectiveness of our method by correcting the bugs in two complex out-of-order superscalar processors with two different timing error recovery mechanisms.

Clock period of pipelined designs are usually determined by the critical paths to avoid timing errors and guarantee reliable operations. The worst case delays of the slowest pipeline stages cause the clock frequency to be less than the average path delays. This may introduce enormous performance loss if the critical paths rarely happen, and the critical path delays are far larger than the average path delays, which is common for many pipelined circuits. In this paper we present a novel timing error recovery technique that guarantees reliable operation of pipelined designs in presence of any arbitrary number of timing errors in different pipeline stages. We allow the clock frequency to be higher than the worst case; hence increasing the performance. We demonstrate the usefulness of our technique by implementing a pipelined arithmetic circuit with the proposed technique on top of a FPGA board. Our experimental results show that we could successfully increase the clock frequency by 30% with the timing error rate of 13%, all of which are automatically corrected with negligible performance penalty. The timing error recovery circuits need extra flipflops for timing error detection and correction. Since typical FPGAs have LUT with flipflops, the extra area for additional flipflops is minimized as the experimental results have shown. With sophisticated synthesis algorithms for pipelined arithmetic circuits which balanced path delays in the circuits, significantly more performance improvements can be expected.

C-based hardware designs are now accepted as means to increase design productivity. Starting with rather algorithmic design descriptions, incremental refinements are applied to generate high-level synhesizable descriptions which are further processed by high-level and logic synthesis tools. C-based system level design descriptions, such as in SpecC [?] and SystemC [?], can give concise and global views on the behaviors of the designs as well as structures, and various types of dependencies, such as control, data, concurrency, and others, can be extracted quickly. These dependencies can be the bases for efficient and effective debugging for all levels of design descriptions. In this paper, graph representations for various dependencies which are extracted from C-based descriptions are introduced. Then techniques on their uses for debugging in various design levels are discussed. We present static and dynamic tracing methods for dependence analysis as well as techniques that try to establish mapping between implementations and C-based design descriptions.

This paper presents a debug method for system communications in post-silicon verification. First, we extract transaction sequences at run-time using on-chip circuits and store them in a trace buffer. Then, we read the stored transactions and analyze them with software. The analysis software tries to find certain patterns in the extracted transactions that are defined by our transaction debug pattern specification language (TDPSL). We have also defined a number of standard patterns for common communication problems such as race and deadlock in TDPSL. To show the feasibility of the method, it is applied to a number of on chip buses. It is shown that the area overhead of the method is very low. Also we have implemented the analysis software and shown that it is memory efficient, scalable and effective to find bugs. The proposed method can also be applied to fault analysis including transient faults.