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.

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 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.

A new simulation scheme of the Digital Spiking Silicon Neuron (DSSN) model is proposed. This scheme is based on the reconfigurable dataflow computing paradigm and targets the Maxeler MaxWorkstation. Compared to the previous implementation of the DSSN network, the new scheme has the virtues of better flexibility and better programmability. More importantly, computing with dataflow cores takes good advantage of the intrinsic parallelism of the reconfigurable hardware and better pipelining is achievable. The proposed scheme has good potential of conducting large-scale and fast simulation of the DSSN-model-based network which is pivotal to future neuroscience research.

In this paper, we present techniques for partial synthesis through sampling mostly for combinational circuits. Here partial synthesis means that most parts of the target circuits are fixed whereas the missing portions must be logic synthesized from scratch. By modeling the missing portions with Look Up Table (LUT) or uninterpreted function (UF), their synthesis and verification problems can be formulated as Quantified Boolean Formulae (QBF). We solve these QBF by repeatedly applying a two step procedure i.e., synthesizing circuits from sample simulation results (necessary conditions) followed by formal verification on the synthesized ones with their specifications for the entire circuits (sufficient conditions). If a circuit is not correct, a counter example is automatically generated which is added to the sampling in the next iteration. With state-of-the-art combinational formal equivalence checkers, our experiments show that large circuits having more than hundreds of thousands of gates can be successfully processed with small numbers of repetitions (in the order of hundreds). Next, we extend the techniques in such a way that no formal specifications nor formal verifiers are available, but only simulation models are used for "correct" partial synthesis. This is achieved by searching for multiple different solution circuits for missing portions which behave the same for the sampled inputs but differently with another input. By repeating this process, we can narrow down the search space, and the solution circuit may become only one which should be the "correct" partial synthesis. We show successfully experimental results with small numbers of repetitions for circuits where 32-inputs/32-outputs sub-circuits are missing.

Statistical model checking is a method to analyze systems where values of variables may have some uncertainty or variations. It can be used to check whether some desired properties are satisfied with specified probability under such uncertainty. In statistical model checking, the system needs to be repeatedly simulated and checked for properties represented in Bounded Linear Temporal Logic (BLTL). The property checking takes a long time if a property includes many variables and/or if the analysis is performed for long sequences. In this paper, we propose a hardware implementation of BLTL property checkers to accelerate the property checking process in statistical model checking. Through the experimental results on Tsunami simulation with variations of earthquake parameters, we show that the total execution time of statistical model checking can be shorten by more than 30 times compared to a software implementation, by implementing our proposed BLTL property checkers on FPGA.

Due to advanced and finer technology, faults in devices can become much more complicated and traditional stuck-at faults may miss important defects. In this paper, we discuss about general functional faults, called “Functionally Observable Fault” (FOF), where the faulty sub-circuit may change its input-output logic functions to any ones. That is, if the faulty sub-circuit has N inputs, faulty behavior can realize as many as (22N- 1) functions. Also, we take care of observability of the functional faults in the sense that non-observable faults from primary outputs are considered as not-faulty. We define FOF and discuss about its Automatic Test Pattern Generation Techniques (ATPG). Although numbers of FOFs can be much more than multiple stuck-at faults for the same sub-circuit, the required numbers of input patterns to detect FOF are not so many compared with multiple stuck-at faults, which suggests practical values of FOF. We show experimental results on ATPG for FOF using ISCAS85 circuits as well as word-level circuits. As our ATPG algorithm processes FOFs in implicit ways, the numbers of test vectors for many multiple FOFs remain small as experimentally shown.

As the verification and debugging of complicated VLSI designs are dominating the chip development time, automated debugging becomes more and more important. In this paper, we propose a method to correct buggy gate-level designs by introducing programmable circuits, such as look up table (LUT) and multiplexer (MUX), that are inserted in order to formulate the debugging processes mathematically. We first replace sets of gates with programmable circuits and try to find a configuration for correction. Some bugs, however, cannot be fixed with only the replacement. In such cases, we add another input to a LUT, where the selection of such additional input is a key for effective debugging. We introduce a necessary condition by which many unusable signals as input to the LUTs can be efficiently eliminated. The experimental results on industrial designs having real bugs show that our proposed method can automatically correct the designs.

Introducing partial programmability in circuits by replacing some gates with look up tables (LUTs) can be an effective way to improve post-silicon or in-field rectification and debugging. Although finding configurations of LUTs that can correct the circuits can be formulated as a QBF problem, solving it by state-of-the-art QBF solvers is still a hard problem for large circuits and many LUTs. In this paper, we present a rectification and debugging method for combinational circuits with LUTs by repeatedly applying Boolean SAT solvers. Through the experimental results, we show our proposed method can quickly find LUT configurations for large circuits with many LUTs, which cannot be solved by a QBF solver.

In modern VLSI designs, assertions play an important role to understand design intention and ensure correctness of designs. In this paper, we consider to generate assertions from simulation results. This assertion extraction is performed by examining whether a logical relation is satisfied among a set of signals. We propose to accelerate it by utilizing a highly parallelized computation performed by GPGPUs. Through the experiments with designs from industry, our implementation on GPGPU runs 30 times faster than a software implementation.

As high-level design draws more attention and has been adopted more widely, verification and debugging for high-level designs has become more important. In this paper, we propose a method to find possible corrections for given counter-examples, targeting high-level design descriptions. To efficiently find corrections, program slicing technique and constraints generated from counterexamples are applied to reduce the number of initial bug candidates and debugging scope. Through the experiments, we show that the proposed method with the reduction efficiently works for several example designs and bugs, and successfully identifies bug locations.

In post-silicon debugging, low observability of internal signal values and large amount of traces are considered as the most critical problems. To address these problems, we propose an on-chip circuitry named DSC (Dynamic Slicing Circuit) which outputs the input signal values that actually influence on an erroneous output value in a particular execution of a chip by analyzing dependencies among signals. Since such input signal values are usually a small subset of the entire input sequence, we can reproduce the error by simulation using them. To realize DSC, we propose a variable named d-tag (Dependency Tag) representing dependency of a signal value with respect to another signal value. For demonstrating our method, we prepared three design examples and implemented DSC circuits on them. As a result, we could successfully extract input signal values that influenced the target output value from a number of random input sequence, for every case. We observed that the number of the extracted input values was significantly smaller than that of the original sequence. The area overhead for DSC circuit were also practical, 4 % in average.

Post-silicon debugging efficiency is getting more critical to shorten the time-to-market than ever, as more bugs escape the verification in pre-silicon phase. Conventionally, simulation of corresponding low-level design description such as RTL or gate-level designs has been used to get observability and controllability. However, the simulation speed of such levels is very slow and the size of design description is very large compared to high-level design. In this paper, we first introduce an approach proposing to debug errors found in post-silicon phase using simulation of high-level designs, instead of low-level designs. To achieve the approach, we propose an I/O sequence mapping method that maps I/O sequences of chip executions to those of the corresponding high-level design. First, we give a formal definition of I/O sequence mapping and relevant notions. Then, based on the definition, we propose an I/O sequence mapping method by executing FSMs representing the interface specifications of the target design. We demonstrate that the proposed method can be effectively applied to several practical design examples with various interfaces.

Fast algorithms and heuristics for real-time object recognition and tracking have enabled a new hybrid world technology in which one can manipulate a real world object and have its virtual world counterpart move correspondingly. This technology has been developed as part of a teaching head platform that was initially designed for language teaching but is now also being used in a range of health-oriented contexts. In this paper, the requirements of the technology are motivated and elucidated, with direct comparison of our proposed heuristics with well known object recognition algorithms.

In this paper, we propose a post-silicon debug framework utilizing high-level design description, which provides great advantage of comprehensibility and readability in analyzing erroneous behaviors for debugging complicated post-silicon errors. The framework consists of the following methods; mapping between high-level and RTL, extracting error-relevant portions, and rank them by the degree of relevance with the error. We also exhibit several experimental results to show its effectiveness.

This paper proposes a new approach for state space exploration on model checking of system-level designs, named "user-driven Breadth-First Search,'' and an interactive verification and debugging environment for its realization. Our approach aims to overcome the limited width of the traditional concrete simulation (Depth-First Search) and the limited depth of symbolic simulation (Breadth-First Search), by combining both of them with the users' guidance. Our case study demonstrates that our approach can detect one of the bugs, which were difficult to be found due to too wide input space for concrete simulation, and due to too deep iteration cycles for symbolic simulation.

We created a human-robot communication system that can adapt to user preferences that can easily change through communication. Even if any learning algorithms are used, evaluating the human-robot interaction is indispensable and difficult. To solve this problem, we installed a machine learning algorithm called interactive evolutionary computation (IEC) into a communication robot named WAMOEBA-3. IEC is a kind of evolutionary computation like a genetic algorithm. With IEC, the fitness function is performed by each user. We carried out experiments on the communication learning system using an advanced IEC system named HMHE. Before the experiments, we did not tell the subjects anything about the robot, so the interaction differed among the experimental subjects. We could observe mutual adaptation, because some subjects noticed the robot's functions and changed their interaction. From the results, we confirmed that, in spite of the changes of the preferences, the system can adapt to the interaction of multiple users