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.

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.

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.

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.