Software-Based Self-Tests (SBST) allow for at-speed testing of on-chip devices via a processor core. However, creating SBSTs requires time-consuming manual labour that is expensive and requires in-depth knowledge of the device’s architecture for targeting hard-to-test faults. Introducing cell-aware testing to this task further exacerbates the necessary effort. In contrast, automating the complex parts of SBST generation using Bounded Model Checking (BMC) allows using sophisticated, state-of-theart BMC solvers to automatically generate vast parts of the SBST. Thereby, a virtual circuit called Validity Checker Module (VCM) is used to encode constraints for the SBST. In this paper, we focus on generating a cell-aware SBST for a Core Local Interrupt Controller (CLIC) that is executed via a RISC-V processor core. We first d erive a constraint s et that creates SBST-like conditions during ATPG, which allows for transformation into instructions later on. We implement a cellaware test model via a re-entrant Mealy state machine that allows complex behaviors of the faulty cell. Experimentally, we extend the CLIC with a test interface that is controlled via a custom CSR of the processor core to reduce SBST generation time and enhance fault coverage. We conclude with the evaluation of our approach on the PULP CLIC implementation that shows cellaware SBST generation to be feasible while achieving acceptable fault coverages and practical generation runtimes.

Graphics Processing Units (GPUs) are becoming widespread, even in safety-critical applications. In that case, it is imperative to guarantee that the probability of producing critical failures due to hardware faults is lower than a given threshold. To detect possible permanent hardware faults as soon as they appear during the operational phase (e.g., due to aging), Software Test Libraries (STLs) have gained significant traction as a widely adopted test solution due to their effectiveness in terms of fault detection capabilities, test application time, and flexibility. However, a major drawback of this solution is the lack of automation in the STL generation phase. As a result, high manual labor is required for their generation. This becomes even more arduous in complex architectures that require in-depth knowledge to cover hard-to-test faults. In this article, we introduce a methodology based on Bounded Model Checking to support the generation and improvement of stuck-at-oriented STLs for hard-to-test units in GPUs, showing that we can enhance the test coverage achieved by pre-existing STLs while also identifying a set of functionally untestable faults. To experimentally validate the proposed method’s effectiveness, we use the FlexGripPlus GPU model to target two hard-to-test units, one medium to low complexity sub-unit and one high complexity sub-unit, as study cases. For both units, we had pre-existing STLs written for the stuck-at model. Resorting to the proposed method, the STLs’ test coverage was increased by 9.57% and 2.19%, respectively. In addition, the method also identified a significant number of functionally untestable faults.

Abstract The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that provably adheres to one or more specifications. Yet, the general problem is undecidable, and policies require full (and thus potentially unbounded) traces of execution history. To provide good approximations of such policies, POMDP agents often employ randomization over action choices. We consider the problem of computing simpler policies for POMDPs, and provide several approaches to still ensure their expressiveness. Key aspects are (1) the combination of an arbitrary number of specifications the policies need to adhere to, (2) a restricted form of randomization, and (3) a light-weight preprocessing of the POMDP model to encode memory. We provide a novel encoding as a mixed-integer linear program as baseline to solve the underlying problems. Our experiments demonstrate that the policies we obtain are more robust, smaller, and easier to implement for an engineer than those obtained from state-of-the-art POMDP solvers.

In-field test of microprocessors is a major topic for the industry, especially in the safety-critical domain, where the respective standards mandate high test coverage thresholds. The dominant fault models used are the transition delay and the stuck-at fault model. However, the adoption of very advanced semiconductor technologies to manufacture devices used in safety-critical applications pushes toward considering new fault models that are better suited to catch subtle and age-related defects. Among the other phenomena, latent cell-internal defects emerged as relevant causes for several failures. Hence, the necessity for the Cell-Aware Test (CAT) was born, and the inclusion of the CAT fault model in the latest safety standards. Although CAT amends the issue of the numerous test escapes, it may suffer as well from the presence of functionally untestable faults that may pollute the overall test efficiency with their presence. In this paper, we propose a solution, based on formal methods, for the automatic identification of functionally untestable faults under the Cell-Aware fault model for the case where the DUT is a fully pipelined processor. As a case study, we used the RISC-V processor RI5CY for which we applied the minimum constraints required to ensure a functional behavior to demonstrate the effectiveness and impact of the approach. With the considered constraints, a significant percentage of functionally untestable faults was located in the several modules within the processor. Furthermore, the method allows to flexibly take into account any constraint stemming from the system configuration and the application. The obtained results have been validated by resorting to commercial EDA tools.

With the continued success of the open RISC-V architecture, practical deployment of RISC-V processors necessitates an in-depth consideration of their testability, safety and security aspects. This survey provides an overview of recent developments in this quickly-evolving field. We start with discussing the application of state-of-the-art functional and system-level test solutions to RISC-V processors. Then, we discuss the use of RISC-V processors for safety-related applications; to this end, we outline the essential techniques necessary to obtain safety both in the functional and in the timing domain and review recent processor designs with safety features. Finally, we survey the different aspects of security with respect to RISC-V implementations and discuss the relationship between cryptographic protocols and primitives on the one hand and the RISC-V processor architecture and hardware implementation on the other. We also comment on the role of a RISC-V processor for system security and its resilience against side-channel attacks.

In the domain of high reliability applications, Burn-In testing (BI) is always present since it is one of the prime countermeasures against the infant mortality phenomenon. Traditional static BI testing proves to be inefficient for modern circuit designs. As the devices’ feature size scales down and their structural and architectural complexity increases, so does the complexity and cost of the BI test. Different BI methods are employed by the industry where stimuli are also applied to the devices under test (DUTs) in order to effectively stress and stimulate all nets of the design. One known industry practice resorts to Design for Testability (DfT) infrastructures (e.g., scan) and is based on the application of test vectors at low frequency to excite the DUT as much as possible with the goal of switching each net of the design at least once. In this paper we consider the case where the layout of the circuit is known and propose two novel methods able to automatically produce functional stimuli to switch pairs of neighboring nodes (i.e., nodes that are placed within a specified distance in the DUT) in short periods of time. This solution has been shown to be able to trigger some latent defects in a circuit better than other methods. As a case study, we target functional units within a RISC-V processor (RI5CY). We show that the functional stimuli generated by the exact method described in the paper are able to achieve optimal results (i.e., the maximum functional switching of neighboring pairs), thus maximizing the chance that their at-speed application can activate weak points in the circuit.

Software-Based Self-Tests (SBST) allow at-speed, native online-testing of processors by running software programs on the processor core, requiring no Design for Testability (DfT) infrastructure. The creation of such SBST programs often requires time-consuming manual labour that is expensive and requires in-depth knowledge of the processor’s architecture to target hard-to-test faults. In contrast, encoding the SBST generation task as a Bounded Model Checking (BMC) problem allows using sophisticated, state-of-the-art BMC solvers to automatically generate an SBST. Constraints for the BMC problem are encoded in a circuit called Validity Checker Module (VCM) and applied during SBST generation.In this paper, we focus on presenting a VCM architecture and a constraint set that allows building SBSTs that make minimal assumptions about the firmware, targeting hard-to-test faults in the ALU and register file of multiple scalar, in-order RISC-V processor families. The VCM architecture consists of a processor-specific mapping layer and a generic constraint set connected via a well-defined interface. The generic constraint set enforces the desired SBST behaviour, including controlling the processor’s pipeline state, memory accesses, and with that executed instructions, register state, and fault propagations. Using a generic constraint set allows for rapid SBST generation targeting new RISC-V processor families while keeping the generic constraints untouched. Lastly, we evaluate this approach on two RISC-V processor families, namely the DarkRISCV and a proprietary, industrial core showing the portability and strength of the approach, allowing for rapidly targeting new processors.

Throughout device testing, one key parameter to be considered is the switching activity (SWA) of the circuit under test (CUT). To avoid unwanted scenarios due to excessive power consumption during test, in most cases the SWA of the CUTs must be retained to a minimal value when the test stimulus is applied. However, there are specific cases where the opposite, namely, the SWA maximization within the CUT, or a certain submodule of it, can be proven beneficial. For example, during dynamic burn-in testing we aim at maximizing the internal stress by applying suitable stimuli. This can be done in a functional manner by following the software-based self-test paradigm. However, generating such suitable programs represents a costly and arduous task for the test engineers. We consider the case where the CUT is a pipelined processor core and we aim to maximize the SWA of certain core submodules. We present a comprehensive methodology based on formal methods, able to automatically generate the best two-instruction stress-inducing sequence for the targeted processor module. The generated stimulus is composed of a short, arbitrarily long repeatable sequence of a pair of assembly instructions, thus, guaranteeing the maximum possible constant SWA. The proposed method was applied to the OpenRISC 1200 and the RI5CY (PULP) processor cores demonstrating its effectiveness when compared to other methods. We show that the time for generating the best repeatable instruction sequence is limited in most cases, while the generated sequence can always achieve a significantly higher repeatable and constant SWA than other solutions.

In this article, we revisit the topic of generalizing proof obligations (POs) in bit-level property directed reachability (PDR). We provide a comprehensive study which: 1) determines the complexity of the problem; 2) thoroughly analyzes limitations of existing methods; 3) introduces approaches to PO generalization that have never been used in the context of PDR; 4) compares the strengths of different methods from a theoretical point of view; and 5) intensively evaluates the methods on various benchmarks from the hardware model checking as well as from AI planning.

Graphics Processing Units (GPUs) boost the development of high-performance safety-critical applications. The reliability of such systems is of utmost importance since faults affecting the hardware may occur at any time during the systems' operational life. Thus, methods to effectively test these devices during their in-field operation are necessary. One popular solution relies on Software Test Libraries (STLs), which recently have been started being used for G PU s as well, since they are effective in terms of fault detection capabilities, intrusiveness, flexibility, and test duration. A drawback of the STL approach for G PU s is the extensive effort used to develop effective test routines for complex structures, e.g., controllers, due to the complicated constraints stemming from the ISA, the available compilation flows and parallelism constraints. We propose a novel technique based on formal methods to support the generation of stimuli and enhance the quality of pre-existing STLs for GPUs. To validate the proposed method, we resort to an open-source GPU model (Flex GripPlu s). Experimental results show that the method can effectively generate complementary code fragments to be added to existing STLs and increase their fault coverage. In the case of the GPU's decoding unit, the stuck-at fault coverage was increased by nearly 10%.

This paper introduces the project Scale4Edge. The project is focused on enabling an effective RISC-V ecosystem for optimization of edge applications. We describe the basic components of this ecosystem and introduce the envisioned demonstrators, which will be used in their evaluation.

During device testing, one of the aspects to be considered is the minimization of the switching activity of the circuit under test in order to steer clear of introducing problems due to device overheating. Nevertheless, there are also certain scenarios during which the maximization of switching activity of the circuit under test (CUT) or of certain parts of it could be proven beneficial e.g., during Burn-In (BI), where internal stress is often produced by applying suitable stimuli. This can be done in a functional manner based on Software-based Self-Test in order to avoid possible damages to the CUT and/or any kind of yield loss. However, the generation of suitable test programs for this task represents a non-trivial task. In this paper we consider a scenario where the circuitry to be stressed is a pipelined processor. We present a methodology, based on formal techniques, able to automatically generate the best functional stress stimuli, i.e., a short and repeatable sequence of assembly instructions, which is guaranteed to induce the maximum switching activity within a given target processor module over a pre-defined time period. For the purposes of our experiments we used the OpenRISC 1200. The gathered experimental results demonstrate the effectiveness of the developed method. In particular, we show that the time for generating the best instruction sequence is limited in most cases, while the generated sequence can always achieve a significantly higher sustained toggling activity than any other solution.

If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.

In several test and reliability problems (from test generation to FMECA and Burn In) it is important to preliminarily identify those lines in a circuit netlist, which can not be controlled, i.e., can not be toggled to both logic values no matter the applied stimuli. Several techniques have been proposed in the past to attack this problem. In this paper we consider the case where the circuit is a pipelined processor, discuss the specific challenges of this scenario and propose some techniques to automatically identify some of the uncontrollable lines. The approach we devised uses SAT solving as underlying technology. We report the results we gathered on the OR1200 processor, showing that our method allows to trade off between the required computational effort and the achieved results. When compared with results produced by a commercial tool, our approach is able to identify a much higher number of uncontrollable lines with reasonable computational requirements.

Reconfigurable Scan Networks (RSNs) allow flexible access to embedded instruments for post-silicon validation and debug or diagnosis. However, the increased observability and controllability can be exploited by an attacker to manipulate or read out sensitive data, if no adequate precautions are taken by the designer. For large RSNs taking those precautions without algorithmic support is virtually impossible. This work proposes a method to automatically generate “minimal witnesses” demonstrating security weaknesses w.r.t. data flow in RSNs. The method provides condensed information to the designer on how to prevent data flow attacks, e.g. by locally modifying the RSN or by preventing active scan paths which contain those minimal witnesses. Experimental results confirm the applicability of the proposed method to diverse benchmark sets, including large designs. Additionally, the benefit of generating “minimal witnesses” for security weaknesses is shown.

Reconfigurable Scan Networks (RSNs) allow flexible access to embedded instruments for post-silicon test, validation and debug or diagnosis. The increased observability and controllability of registers inside the circuit can be exploited by an attacker to leak or corrupt critical information.Precluding such security threats is of high importance but difficult due to complex data flow dependencies inside the reconfigurable scan network as well as across the underlying circuit logic.This work proposes a method that fine-granularly computes dependencies over circuit logic and the RSN. These dependencies are utilized to detect security violations for a given insecure RSN, which is then transformed into a secure RSN.Experimental results demonstrate the applicability of the method to large academical and industrial designs. Additionally, we report on the required effort to mitigate found security violations which also motivates the necessity to consider the circuit logic in addition to pure scan paths.

Reconfigurable Scan Networks (RSNs) are a powerful tool for testing and maintenance of embedded systems, since they allow for flexible access to on-chip instrumentation such as built-in self-test and debug modules. RSNs, however, can be also exploited by malicious users as a side-channel in order to gain information about sensitive data or intellectual property and to recover secret keys. Hence, implementing appropriate counter-measures to secure the access to and data integrity of embedded instrumentation is of high importance. In this paper we present a novel hardware and software combined approach to ensure data privacy in IEEE Std 1687 (IJTAG) RSNs. To do so, both a secure IJTAG compliant plug-and-play instrument wrapper and a versatile software toolchain are introduced. The wrapper demonstrates the necessary architectural adaptations required when using a lightweight stream cipher, whereas the software toolchain provides a seamless integration of the testing workflow with stream cipher. The applicability of the method is demonstrated by an FPGA-based implementation. We report on the performance of the developed instrument wrapper, which is empirically shown to have only a small impact on the workflow in terms of hardware overhead, operational costs and test time overhead.

We present a novel FPGA based active stereo vision system, tailored for the use in a mobile 3D stereo camera. For the generation of a single 3D map the matching algorithm is based on a correlation approach, where multiple stereo image pairs instead of a single one are processed to guarantee an improved depth resolution. To efficiently handle the large amounts of incoming image data we adapt the algorithm to the underlying FPGA structures, e.g. by making use of pipelining and parallelization.Experiments demonstrate that our approach provides high-quality 3D maps at least three times more energy-efficient (5.5 fps/W) than comparable approaches executed on CPU and GPU platforms. Implemented on a Xilinx Zynq-7030 SoC our system provides a computation speed of 12.2 fps, at a resolution of 1.3 megapixel and a 128 pixel disparity search space. As such it outperforms the currently best passive stereo systems of the Middlebury Stereo Evaluation in terms of speed and accuracy. The presented approach is therefore well suited for mobile applications, that require a highly accurate and energy-efficient active stereo vision system.

The evaluation of fault attacks on security-critical hardware implementations of cryptographic primitives is an important concern. In such regards, we have created a framework for automated construction of fault attacks on hardware realization of ciphers. The framework can be used to quickly evaluate any cipher implementations, including any optimisations. It takes the circuit description of the cipher and the fault model as input. The output of the framework is a set of algebraic equations, such as conjunctive normal form (CNF) clauses, which is then fed to a SAT solver. We consider both attacking an actual implementation of a cipher on an field-programmable gate array (FPGA) platform using a fault injector and the evaluation of an early design of the cipher using idealized fault models. We report the successful application of our hardware-oriented framework to a collection of ciphers, including the advanced encryption standard (AES), and the lightweight block ciphers LED and PRESENT. The corresponding results and a discussion of the impact to different fault models on our framework are shown. Moreover, we report significant improvements compared to similar frameworks, such as speedups or more advanced features. Our framework is the first algebraic fault attack (AFA) tool to evaluate the state-of-the art cipher LED-64, PRESENT and full-scale AES using only hardware-oriented structural cipher descriptions.

We study strategy synthesis for partially observable Markov decision processes (POMDPs). The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train a recurrent neural network (RNN) to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes.

Hardware security adds another dimension to the design space, and more and more attention is paid to protect a circuit against various types of attacks like sniffing, spoofing or IP theft. However, all the efforts for security taken by a designer might be sacrificed by afterwards integrating infrastructure for test, diagnosis and reliability management. Especially, access mechanisms like reconfigurable scan networks (RSNs) may open options for side-channel attacks. Using the presented approach an accurate estimation of reachability properties of all considered benchmarks is provided. The method uses a matrix-based reachability analysis of the original design and the augmented design. The reachability analysis covers complex functional dependencies, caused by configuring a single scan path as well as multiple sequentially activated scan paths through the RSN. This approach adds acceptable runtime to the security verification flow of the design, and shows the designer the introduced possible security violations.

With ever more complex and larger VLSI devices and higher and higher reliability requirements, high quality test with a large fault and defect coverage is becoming even more relevant. At the same time, when unspecified or unknown input values (X values) have to be considered in a pattern, commercial ATPG tools are sometimes not capable of determining whether a fault can be tested - but there is at least a chance to detect the fault, as 0/X or 1/X could be propagated to at least one output. Consequently, these faults are considered to be possibly detected and often counted towards the overall fault coverage with a weighting factor. However, as the actual probability to detect these faults with the considered test pattern is not taken into account, this could lead to an over-or underestimation of their real fault coverage, falsifying the test results. We introduce a #SAT-based characterization algorithm for this class of faults. This new algorithm is, for the first time, able to accurately compute the detection probability for faults marked as possibly detected by state-of-the-art commercial tools. Our experimental results for the largest ITC'99 benchmarks as well as larger industrial-circuits show that our algorithm can accurately determine the detection probability for most of the possibly detected faults and also identify faults that are completely untestable or found with a probability of 100 % irrespective of the assignment of the inputs with an X value. Furthermore, they show that the detection probability is circuit-dependent and consequently should not just be estimated by a simple weighting factor but requires a more in-depth evaluation. Otherwise, there is a high risk that the achieved results could clearly be to optimistic or pessimistic with regard to the real fault coverage.

Modern systems-on-chip (SoC) designs are requiring more and more infrastructure for validation, debug, volume test as well as in-field maintenance and repair. Reconfigurable scan networks (RSNs), as allowed by IEEE 1687 (IJTAG) standard, provide flexible access to the infrastructure with low access latency. However, they can also pose a security threat to the system, by leaking information about the system state. In this paper, we present a protection method that monitors access and checks for violations of security properties online. The method prevents unauthorized access to sensitive and secure instruments. In addition, the system integrator can specify more complex security requirements, including giving multiple users different access privileges. Simultaneous accesses to multiple instruments, that would expose sensitive data to an untrusted core (e.g. from 3rd party vendors) or instrument, can be prohibited. The method does not require any change to the RSN architecture and is easily integrable with IP core designs. The area overhead with respect to the size of the RSN is below 6% and scales well with larger networks.

Vulnerabilities and design flaws in Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constraint the sensitive communication inside the Multi-Processors Systems-on-Chip (MPSoCs). Although previous works address the NoC threat, finding secure and efficient solutions to verify the security is still a challenge. In this work, we propose for the first time a method to formally verify the correctness and the security properties of a NoC router in order to provide the proper communication functionality and to avoid NoC attacks. We present a generalized verification flow that proves a wide set of implementation-independent security-related properties to hold. We employ unbounded model checking techniques to account for the highly-sequential behaviour of the NoC systems. The evaluation results demonstrate the feasibility of our approach by presenting verification results of six different NoC routing architectures demonstrating the vulnerabilities of each design.

Reconfigurable Scan Networks (RSNs) allow flexible access to embedded instruments for post-silicon validation and debug or diagnosis. However, this scan infrastructure can also be exploited to leak or corrupt critical information as observation and controllability of registers deep inside the circuit are increased. Securing an RSN is mandatory for maintaining safe and secure circuit operations but difficult due to its complex data flow dependencies. This work proposes a method that detects security violations and transforms a given insecure RSN into a secure RSN for which the secure data flow as specified by a user is guaranteed by construction. The presented method is guided by user-defined cost functions that target e.g., test performance or wiring cost. We provide a case study and experimental results demonstrating the applicability of the method to large designs with low runtime.

The characterization of analog-mixed signal (AMS) silicon requires a suitable pattern set able to exercise the parametric operational space to - among other tasks - validate the correct (specified) working behaviour of the device under test. As experience shows, most of the unexpected problems occur for very specific value combinations of a few test condition variables that were not expected to have an influence. Additionally, restrictions on the operational conditions have to be taken into account. We present a method to efficiently create a set of test conditions to cover such a constrained search space with a user-defined density. First, an initial test condition set is generated using quasirandom Sobol sequences. Secondly, we analyse the test conditions to identify and fill uncovered areas in the parameter space using the in-house interval constraint solver iSAT3. The applicability of the method is demonstrated by experimental results on a 19-dimensional search space using a realistic set of constraints.

Opens are known to be one of the predominant defects in nanoscale technologies. With an increasing number of complex cells in today's very large-scale integration designs intracell opens are becoming a larger and larger problem. Typically, these defects are modeled by transistor stuck-off faults (TSOFs) and assumed to be detected by transition delay fault (TDF) timing tests. However, tests for TDF fail to detect a high percentage of TSOFs and even tools that target them directly are not sufficient to screen all open defects. Furthermore, generated tests might be invalidated in case hazards and charge-sharing are not properly considered. In this paper, we present a waveform-accurate SAT-based automatic test pattern generation (ATPG) framework to tackle these problems. The proposed method not only allows for the generation of tests that are robust against hazards and charge-sharing, it can also be used to generate tests for faults only detectable by hazard-based activation-and hence even increase the fault coverage beyond state-of-the-art cell-aware tests. Our experimental results for the largest ITC'99, IWLS 2005 as well as larger industrial circuits mapped to the state-of-the-art NanGate 45-nm as well as NanGate 15-nm cell library using complex cells show the high efficiency and scalability of the proposed method. For example, the results show that without properly considering hazards and charge-sharing up to 17.9% of the generated tests could be invalidated. In addition, hazard-activated ATPG allows to detect an additional 10.1% of conventionally undetectable faults that could result in a very significant defective parts per million improvement.

Opens are known to be one of the predominant defects in nanoscale technologies. Especially with an increasing number of complex cells in today's VLSI designs intra-gate opens are becoming a major problem. The generation of tests for these faults is hard, as the timing of the circuit needs to be considered accurately to prevent the invalidation of the generated tests through hazards. Current test generation methods, including new cell aware tests that explicitly target open defects, ignore the possibility of hazard caused test invalidation. Such tests can fail to detect a significant fraction of the targeted opens. In this work we present a waveform-accurate hazard-aware test generation approach to target intra-gate opens. Our methodology is based on a SAT-based encoding and allows the generation of tests guaranteed to be robust against hazards. Experimental results for large benchmarks mapped to the state-of-the-art NanGate 45nm cell library including complex cells show the test generation efficiency of the proposed method. Large circuits were efficiently handled - even without the use of fault simulation. Our experiments show that on average, about 10.92 % of conventional hazard-unaware tests will fail to detect the targeted opens because of test invalidation - these are reliably detected by our new test generation methodology. Importantly, our approach can also be applied to improve the effectiveness of commercial cell aware tests.

Physical unclonable functions (PUFs) can be used for a number of security applications, including secure on-chip generation of secret keys. We introduce an embedded PUF concept called sensitized path PUF (SP-PUF) that is based on extracting entropy out of inherent timing variability of modules already present in the circuit. The new PUF sensitizes paths of nearly identical lengths and generates response bits by racing transitions through different paths against each other. SP-PUF has lower area overhead and higher speed than earlier embedded PUFs and requires no helper data stored in non-volatile memory beyond standard error-correction information for fuzzy extraction. Compared with standalone PUFs, the new solution intrinsically and inseparably intertwines PUF behavior with functional circuitry, thus complicating invasive attacks or simplifying their detection. We present a systematic design flow to turn an arbitrary (sufficiently complex) circuit into an SP-PUF. The flow leverages state-of-the-art sensitization algorithms, formal filtering based on statistical analysis, and MaxSAT-based optimization of SP-PUF's area overhead. Experiments show that SP-PUF extracts 256-bit keys with perfect reliability and nearly perfect uniqueness after fuzzy extraction for the majority of standard benchmark circuits.

The European Test Symposium (ETS) Best Paper Award, which was introduced in 2004 when the European Test Workshop (ETW) turned into the ETS, aims to maintain and encourage the quality of papers and presentations in the ETS technical program.

A large amount of on-chip infrastructure, such as design-for-test, debug, monitoring, or calibration, is required for the efficient manufacturing, debug, and operation of complex hardware systems. The access to such infrastructure poses severe system safety and security threats since it may constitute a side-channel exposing internal state, sensitive data, or IP to attackers. Reconfigurable scan networks (RSNs) have been proposed as a scalable and flexible scan-based access mechanism to on-chip infrastructure. The increasing number and variety of integrated infrastructure as well as diverse access constraints over the system lifetime demand for systematic methods for the specification and formal verification of access protection and security properties in RSNs. This work presents a novel method to specify and verify fine-grained access permissions and restrictions to instruments attached to an RSN. The permissions and restrictions are transformed into predicates that are added to a formal model of a given RSN to prove which access properties hold or do not hold.

A prototype of the framework AutoFault, which automatically constructs fault-injection attacks for hardware realizations of ciphers, is presented. AutoFault can be used to quickly evaluate the resistance of security-critical hardware blocks to fault attacks and the adequacy of implemented countermeasures. The framework takes as inputs solely the circuit description of the cipher and the fault(s) and produces an algebraic formula that can be handed over to an external solver. In contrast to previous work, attacks constructed by AutoFault do not incorporate any cipher-specific cryptoanalytic derivations, making the framework accessible to users without cryptographic background. We report successful application of AutoFault in combination with a state-of-the-art SAT solver to LED-64 and to small-scale AES. To the best of our knowledge, this is the first time that a state-of-the-art cipher (LED-64) was broken by a fault attack with no prior manual cryptanalysis whatsoever.

With an increasing number of complex cells in today's VLSI designs, intra-gate opens are becoming a larger and larger problem. Typically, these defects are modeled by transistor stuck-off faults (TSOF) and assumed to be detected by transition delay fault (TDF) timing tests. However, tests for TDF fail to detect a high percentage of TSOFs and even tools that target them directly are not sufficient to screen all open defects. This is because CMOS circuits experience a large number of hazards during circuit inputs switching which are not modeled by classical tools. Hazards may activate some TSO faults considered untestable by classical ATPGs. The generation of tests that target such hazard activated opens can result in a very significant DPPM improvement - if used. In this paper, we present the first deterministic methodology for targeting hazard activated opens. It is based on a waveform-accurate SAT-based modeling and allows to accurately determine if a TSOF is detectable by hazard activation - or not. In addition, we provide a thorough investigation of the additionally achievable fault coverage using the state-of-the-art NanGate 45nm as well as NanGate 15nm cell libraries.

Abstract Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.

Unknown (X) values in a design introduce pessimism in conventional test generation algorithms, which results in a loss of fault coverage. This pessimism is reduced by a more accurate modeling and analysis. Unfortunately, accurate analysis techniques highly increase runtime and limit scalability. One promising technique to prevent high runtimes while still providing high accuracy is the use of restricted symbolic logic (RSL). However, also pure RSL-based algorithms reach their limits as soon as millon gate circuits need to be processed. In this paper, we propose new ATPG techniques to overcome such limitations. An efficient hybrid encoding combines the accuracy of RSL-based modeling with the compactness of conventional threevalued encoding. A low-cost two-valued SAT-based untestability check is able to classify most untestable faults with low runtime. An incremental and event-based accurate fault simulator is introduced to reduce fault simulation effort. The experiments demonstrate the effectiveness of the proposed techniques. On average, over 99.3% of the considered faults are accurately classified. Both the number of aborts and the total runtime are significantly reduced compared to the state-of-the-art pure RSL-based algorithm. For circuits up to a million gates, the fault coverage could be increased considerably compared to a state-of-the-art commercial tool with very competitive runtimes.

Detailed knowledge of a circuit's timing is essential for performance optimization, timing closure, and generation of test patterns to detect small-delay defects. When an input transition is applied to the circuit's inputs, the resulting delay is not only determined by the propagation path, but also influenced by the power-supply noise. We introduce a path-sensitization procedure which precisely controls the switching activity in the circuit region surrounding the path. The procedure can maximize or minimize switching activity, or set it to a user-specified value. We study the accuracy-vs.-efficiency trade-offs for a hierarchy of timing models, from coarse zero-delay assumption to a waveform-accurate approach with sub-cycle resolution. For the first time, we present a MaxSAT formulation which guarantees maximization or minimization of switching activity, stemming from transitions and from glitches, simultaneously with path sensitization. We validate the quality of the generated test patterns using a mixed-mode IR-drop-aware timing simulator.

The #SAT problem, that is counting the number of solutions of a propositional formula, extends the well-known SAT problem into the realm of probabilistic reasoning. However, the higher computational complexity and lack of fast solvers still limits its applicability for real world problems. In this work we present our distributed parallel #SAT solver dCountAntom which utilizes both local, shared-memory parallelism as well as distributed (cluster computing) parallelism. Although highly parallel solvers are known in SAT solving, such techniques have never been applied to the #SAT problem. Furthermore we introduce a solve progress indicator which helps the user to assess whether the presented problem is likely solvable within a reasonable time. Our analysis shows a high accuracy of the estimated progress. Our experiments with up to 256 CPU cores working in parallel yield large speedups across different benchmarks derived from real world problems: With the maximum number of available cores dCountAntom solved problems on average 141 times faster than a single core implementation.

Reconfigurable scan networks (RSN) as standardized by IEEE Std 1687 allow flexible and efficient access to on-chip infrastructure for test and diagnosis, post-silicon validation, debug, bring-up, or maintenance in the field. However, unauthorized access or manipulation of the attached instruments, monitors, or controllers pose security and safety risks. Different RSN architectures have recently been proposed to implement secure access to the connected instruments, for instance by authentication and authorization. To ensure that the implemented security schemes cannot be bypassed, design verification of the security properties is mandatory. However, combinational and deep sequential dependencies of modern RSNs and their extensions for security require novel approaches to formal verification for unbounded model checking. This work presents for the first time a formal design verification methodology for security properties of RSNs based on unbounded model checking that is able to verify access protection at logical level. Experimental results demonstrate that state-of-the-art security schemes for RSNs can be efficiently handled, even for very large designs.

In scientific and technical software, floating-point arithmetic is often used to approximate arithmetic on physical quantities natively modeled as reals. Checking properties for such programs (e.g. proving unreachability of code fragments) requires accurate reasoning over floating-point arithmetic. Currently, most of the SMT-solvers addressing this problem class rely on bit-blasting. Recently, methods based on reasoning in interval lattices have been lifted from the reals (where they traditionally have been successful) to the floating-point numbers. The approach presented in this paper follows the latter line of interval-based reasoning, but extends it by including bitwise integer operations and cast operations between integer and floating-point arithmetic. Such operations have hitherto been omitted, as they tend to define sets not concisely representable in interval lattices, and were consequently considered the domain of bit-blasting approaches. By adding them to interval-based reasoning, the full range of basic data types and operations of C programs is supported. Furthermore, we propose techniques in order to mitigate the problem of aliasing during interval reasoning. The experimental results confirm the efficacy of the proposed techniques. Our approach outperforms solvers relying on bit-blasting as well as the existing interval-based SMT-solver.

Functional test and software-based self-test (SBST) approaches for processors are becoming popular as they enable low-cost production tests and are often the only solution for in-field tests. With the increasing use of volume diagnosis, efficient and cost-effective diagnosis methods are required. A high quality functional or SBST test program can be used to perform logic fault diagnosis with low-cost test equipment and therefore significantly reduce the cost of diagnosis. We present a framework for the automatic generation of functional diagnostic sequences for stuck-at faults. The framework allows a user to specify constraints imposed by the employed test environment and generates diagnostic sequences satisfying these constraints. Furthermore, the framework is able to prove the equivalence of faults under the specified constraints. This enables to compute the best possible diagnostic quality that can be reached under the given environmental constraints. Also, it gives the necessary information for implementing selective DFT techniques in order to differentiate faults which cannot be distinguished otherwise. In our experiments we evaluated a MIPS-like processor. The results show that our approach can effectively distinguish fault pairs or prove their equivalence, under different environmental constraints. To the best, of our knowledge, this is the first approach which, enables the automatic generation of diagnostic SBST, programs and allows to eectively prove the equivalence of faults in functional and SBST test environments.

Knowledge about sensitizable paths through combinational logic is essential for numerous design tasks. We present the framework PHAETON which identifies sensitizable paths and generates test pairs to exercise these paths using Boolean satisfiability (SAT). PHAETON supports a large number of models and sensitization conditions and provides a generic interface that can be used by applications. It incorporates a novel application-specific unary representation of integer numbers to integrate timing information with logical conditions within the same monolithic SAT formula. Due to a number of further elaborate speed-up techniques, PHAETON scales to industrial circuits. Experimental results show the performance of PHAETON in classical K longest path generation tasks and in new post-silicon validation and characterization scenarios.

Software-based self-test (SBST) techniques are used to test processors and processor cores against permanent faults introduced by the manufacturing process or to perform in-field test in safety-critical applications. However, the generation of an SBST program is usually associated with high costs as it requires significant manual effort of a skilled engineer with in-depth knowledge about the processor under test. In this paper, we propose an approach for the automatic generation of SBST programs. First, we detail an automatic test pattern generation (ATPG) framework for the generation of functional test sequences. Second, we describe the extension of this framework with the concept of a validity checker module (VCM), which allows the specification of constraints with regard to the generated sequences. Third, we use the VCM to express typical constraints that exist when SBST is adopted for in-field test. In our experimental results, we evaluate the proposed approach with a microprocessor without interlocked pipeline stages (MIPS)-like microprocessor. The results show that the proposed method is the first approach able to automatically generate SBST programs for both end-of-manufacturing and in-field test whose fault efficiency is superior to those produced by state-of-the-art manual approaches.

Physically unclonable functions (PUFs) based on ring oscillators (ROs) are a popular primitive in hardware security, meant to enable the unambiguous and tamper-proof identification of computer chips. This is achieved by exploiting different signal delays on each chip stemming from uncontrollable variations during the manufacturing process. Thus, the relation between RO frequencies on an individual chip can be used as the chip's unique PUF signature. In this work, we show how ROs implemented on a larger number of Altera Cyclone IV FPGAs are biased towards slower or faster frequencies in non-uniform ways depending on the FPGA's programming with different design; even though the ROs are placed and routed equally. Without considering these biases, inter-device uniqueness of the PUF signatures is degraded. We demonstrate that subtracting the mean frequency of each RO - derived using only a small training set of devices - from the sampled frequencies overcomes this disadvantage; i.e. the uniqueness is increased drastically while maintaining reliability.

Power-related problems in at-speed scan testing have become more and more serious, since excessive IR-drop caused by excessive power consumption results in overtesting. There are two important factors in low-power testing: one is power estimation, the other is power reduction. Several estimation methods have been proposed based on the analysis of switching activity characteristics. In order to estimate the impact of IR-drop, it is more important to consider the area containing many cells which consume excessive power than to consider the total number of switching activity in a circuit. In this paper, we propose a novel method for identifying areas where excessive IR-drop likely occurs without using test vectors. Visualized experimental results for IWLS 2005 benchmark circuits demonstrate that the proposed method can effectively identify areas containing many cells which consume higher power than others. Such areas identified can be used in low-power test generation so as to achieve effective and efficient results.

Test generation algorithms considering unknown (X) values are pessimistic if standard n-valued logic algebras are used. This results in an overestimation of the number of signals with X-values and an underestimation of the fault coverage. In contrast, algorithms based on quantified Boolean formula (QBF), are accurate in presence of X-values but have limits with respect to runtime, scalability and robustness. Recently, an algorithm based on restricted symbolic logic (RSL) has been presented which is more accurate than classical three-valued logic and faster than QBF. Nonetheless, this RSL-based approach is still pessimistic and is unable to detect all testable faults. Additionally, it does not allow the accurate identification of untestable faults. In this paper, we improve test pattern generation based on RSL in two directions in order to reduce the accuracy-gap to QBF further. First, we present techniques to go beyond the accuracy of RSL when generating test patterns. Second, we include a check which is able to accurately identify untestable faults. Experimental results show the high efficiency of the proposed method. It is able to classify almost all faults - either by generating a test pattern or proving untestability.

Interconnect opens are known to be one of the predominant defects in nanoscale technologies. Generating tests to detect such defects is challenging due to the need to accurately determine the coupling capacitances between the open net and its aggressors and fix the state of these aggressors during test. Process variations cause deviations from assumed values of circuit parameters thus potentially invalidating tests generated with assumed circuit parameters. Additionally, recent investigation using test chips showed that the steady state voltage on open nets may drift slowly with the application of circuit inputs and can be different at different nets.

Manufactured VLSI circuits using a new technology typically suffer from systematic defects that are process-dependent and at sub-nanometer feature sizes such defects may be even design-dependent. The root causes for systematic defects must be determined to ramp up yields. Volume diagnosis is becoming popular to identify root causes for systematic defects. Volume diagnosis uses logic diagnosis based on failing circuit responses to production tests of a large number of failing devices, followed by statistical analysis methods to determine the root cause(s) for yield limiters. Typically production tests use fault detection tests and hence may have limited diagnosis resolution. To improve diagnosis resolution diagnostic ATPGs can be used to generate test sets to distinguish all pairs of distinguishable faults in one or more fault models. The sizes of such tests tend to be considerably higher than fault detection test sets used as production tests. For this reason, generation of test sets that detect faults and also possess a high diagnosis resolution is important. In this work we present a method to improve the diagnosis resolution of a compact fault detection test set without increasing pattern count or decreasing fault coverage. The basic idea of the approach is to generate a SAT formula which enforces diagnosis and is solved by a MAX-SAT solver which is a SAT-based maximization tool. We believe this is the first time a method to improve diagnosis resolution of a test set of given size has been reported. Experimental results on ISCAS 89 circuits demonstrate the effectiveness of the proposed method.

Unknown (X) values emerge during the design process as well as during system operation and test application. X-sources are for instance black boxes in design models, clock-domain boundaries, analog-to-digital converters, or uncontrolled or uninitialized sequential elements. To compute a test pattern for a given fault, well-defined logic values are required both for fault activation and propagation to observing outputs. In presence of X-values, conventional test generation algorithms, based on structural algorithms, Boolean satisfiability (SAT), or binary decision diagram-based reasoning may fail to generate test patterns or to prove faults untestable. This paper proposes the first efficient stuck-at and transition-delay fault test generation algorithm able to prove testability or untestability of faults in presence of X-values. It overcomes the principal pessimism of conventional algorithms when X-values are considered by mapping the test generation problem to the SAT of quantified Boolean formulas. Experiments on ISCAS benchmarks and larger industrial circuits investigate the increase in fault coverage for conventional deterministic and potential detection requirements for both randomized and clustered X-sources.

Vulnerability to malicious fault attacks is an emerging concern for hardware circuits that are employed in mobile and embedded systems and process sensitive data. We describe a new methodology to assess the vulnerability of a circuit to such attacks, taking into account built-in protection mechanisms. Our method is based on accurate modeling of fault effects and detection status expressed by Boolean satisfiability (SAT) formulas. Vulnerability is quantified based on the number of solutions of these formulas, which are determined by an efficient #SAT solver. We demonstrate the applicability of this method for design space exploration of a pseudo random number generator and for calculating the attack success rate in a multiplier circuit protected by robust error-detecting codes.

We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of reliability analysis, e.g., of computer network performability analysis, of power grids, of computer virus vulnerability, and in the study of crowd dynamics. We use abstraction techniques together with novel algorithms for the computation of bounds on the expected final and accumulated rewards in continuous-time Markov decision processes (CTMDPs). These ingredients are combined in a partly symbolic and partly explicit (symblicit) analysis approach. In particular, we circumvent the use of multi-terminal decision diagrams, because the latter do not work well if facing a large number of different rates. We demonstrate the practical applicability and efficiency of the approach on two case studies.

Open defects such as interconnect opens are known to be one of the predominant defects in nanoscale technologies. Yet, test pattern generation for open defects is challenging because of the high number of parameters which need to be considered. Additionally, the assumed values of these parameters may vary due to process variations reducing fault coverage of a test set generated under this assumption. This paper presents a new ATPG approach for circuit Parameter independent (CPI) tests. In addition a definition of oscillation free CPI tests is given. The generated tests are robust against process variations affecting the influence of neighboring interconnects as well as trapped charge and prohibit oscillating behavior. Experimental results show the high efficiency of the new approach, generating CPI tests for circuits with over 500k nonequivalent faults and several thousand aggressors.

Interconnect opens are known to be one of the predominant defects in nanoscale technologies. However, automatic test pattern generation for open faults is challenging, because of their rather unstable behaviour and the numerous electric parameters which need to be considered. Thus, most approaches try to avoid accurate modeling of all constraints and use simplified fault models in order to detect as many faults as possible or make assumptions which decrease both complexity and accuracy. This paper presents a new SMT-based approach which for the first time supports the Robust Enhanced Aggressor Victim model without restrictions and handles oscillations. It is combined with the first open fault simulator fully supporting the Robust Enhanced Aggressor Victim model and thereby accurately considering unknown values. Experimental results show the high efficiency of the new method outperforming previous approaches by up to two orders of magnitude.

In this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach.

Functional microprocessor test methods provide several advantages compared to DFT approaches, like reduced chip cost and at-speed execution. However, the automatic generation of functional test patterns is an open issue. In this work we present an approach for the automatic generation of functional microprocessor test sequences for small-delay faults based on Bounded Model Checking. We utilize an ATPG framework for small-delay faults in sequential, non-scan circuits and propose a method for constraining the input space for generating functional test sequences (i.e., test programs). We verify our approach by evaluating the miniMIPS microprocessor. In our experiments we were able to reach over 97 % fault efficiency. To the best of our knowledge, this is the first fully automated approach to functional microprocessor test for small-delay faults.

In technologies affected by variability, the detection status of a small-delay fault may vary among manufactured circuit instances. The same fault may be detected, missed or provably undetectable in different circuit instances. We introduce the first complete flow to accurately evaluate and systematically maximize the test quality under variability. As the number of possible circuit instances is infinite, we employ statistical analysis to obtain a test set that achieves a fault-efficiency target with an user-defined confidence level. The algorithm combines a classical path-oriented test-generation procedure with a novel waveform-accurate engine that can formally prove that a small-delay fault is not detectable and does not count towards fault efficiency. Extensive simulation results demonstrate the performance of the generated test sets for industrial circuits affected by uncorrelated and correlated variations.

This work is motivated by (1) a practical application which automatically generates test patterns for integrated circuits and (2) the observation that off-the-shelf state-of-the-art pseudo-Boolean solvers have difficulties in solving instances with huge pseudo-Boolean constraints as created by our application. Derived from the SMT solver iSAT3 we present the solver iSAT3p that on the one hand allows the efficient handling of huge pseudo-Boolean constraints with several thousand summands and large integer coefficients. On the other hand, experimental results demonstrate that at the same time iSAT3p is competitive or even superior to other solvers on standard pseudo-Boolean benchmark families.

Test generation algorithms based on standard n-valued logic algebras are pessimistic in presence of unknown (X) values, overestimate the number of signals with X-values and underestimate fault coverage.

Logic and fault simulation are essential techniques in electronic design automation. The accuracy of standard simulation algorithms is compromised by unknown or X-values. This results in a pessimistic overestimation of X-valued signals in the circuit and a pessimistic underestimation of fault coverage. This work proposes efficient algorithms for combinational and sequential logic as well as for stuck-at and transition-delay fault simulation that are free of any simulation pessimism in presence of unknowns. The SAT-based algorithms exactly classifiy all signal states. During fault simulation, each fault is accurately classified as either undetected, definitely detected, or possibly detected. The pessimism with respect to unknowns present in classic algorithms is thoroughly investigated in the experimental results on benchmark circuits. The applicability of the proposed algorithms is demonstrated on larger industrial circuits. The results show that, by accurate analysis, the number of detected faults can be significantly increased without increasing the test-set size.

Circuits that employ test pattern compression rely on test cubes to achieve high compression ratios. The less inputs of a test pattern are specified, the better it can be compacted and hence the lower the test application time. Although there exist previous approaches to generate such test cubes, none of them are optimal. We present for the first time a framework that yields provably optimal test cubes by using the theory of quantified Boolean formulas (QBF). Extensive comparisons with previous methods demonstrate the quality gain of the proposed method.

Unknown (X) values in a circuit impair test quality and increase test costs. Classical n-valued algorithms for fault simulation and ATPG, which typically use a three- or four-valued logic for the good and faulty circuit, are in principle pessimistic in presence of X-values and cannot accurately compute the achievable fault coverage. In partial scan or pipelined circuits, X-values originate in non-scan flip-flops. These circuits are tested using multi-cycle tests. Here we present multi-cycle test generation techniques for circuits with X-values due to partial scan or other X-sources. The proposed techniques have been integrated into a multi-cycle ATPG framework which employs formal Boolean and quantified Boolean (QBF) satisfiability techniques to compute the possible signal states in the circuit accurately. Efficient encoding of the problem instance ensures reasonable runtimes. We show that in presence of X-values, the detection of stuck-at faults requires not only exact formal reasoning in a single cycle, but especially the consideration of multiple cycles for excitation of the fault site as well as propagation and controlled reconvergence of fault effects. For the first time, accurate deterministic ATPG for multi-cycle test application is supported for stuck-at faults. Experiments on ISCAS'89 and industrial circuits with X-sources show that this new approach increases the fault coverage considerably.

Ongoing research to shrink feature sizes of LSI circuits leads to an always increasing number of logic gates in a circuit. In general, the complexity of test generation depends on the size of a circuit. Furthermore, modern test generation methods have to consider power reduction in addition to fault detection, since excessive power caused by testing may result in over testing. In this work, we propose a method to reduce the computation time of low-power test generation. The proposed method specifies gates which will cause power issues, consequently reducing the search space for X-filling technique. The reduction of search space for Xfilling also further minimizes the amount of switching activity. Experimental results for circuits of Open Cores provided by IWLS2005 benchmarks show that the proposed method achieves both a reduced computation time and at the same time increased power reduction compared to previous methods.

Unknown (X) values may emerge during the design process as well as during system operation and test application. Sources of X-values are for example black boxes, clock-domain boundaries, analog-to-digital converters, or uncontrolled or uninitialized sequential elements.

Comprehensive coverage of small-delay faults under massive process variations is achieved when multiple paths through the fault locations are sensitized by the test pair set. Using one test pair per path may lead to impractical test set sizes and test application times due to the large number of near-critical paths in state-of-the-art circuits.

We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.

Early-life failures (ELF) result from weak chips that may pass manufacturing tests but fail early in the field, much earlier than expected product lifetime. Recent experimental studies over a range of technologies have demonstrated that ELF defects result in changes in delays over time inside internal nodes of a logic circuit before functional failure occurs. Such changes in delays are distinct from delay degradation caused by circuit aging mechanisms such as Bias Temperature Instability. Traditional transition fault or robust path delay fault test patterns are inadequate for detecting such ELF-induced changes in delays because they do not model the demanding detection conditions precisely. In this paper, we present an automatic test pattern generation (ATPG) technique based on Boolean Satisfiability (SAT) for detecting ELF-induced delay changes at all gates in a given circuit. Our simulation results, using various circuit blocks from the industrial OpenSPARC T2 design as well as standard benchmarks, demonstrate the effectiveness and practicality of our approach in achieving high coverage of ELF-induced delay change detection. We also demonstrate the robustness of our approach to manufacturing process variations.

The shrinking nanometer technologies of modern microprocessors and the aggressive supply voltage down-scaling drastically increase the risk of soft errors. In order to cope with this risk efficiently, selective hardware and software protection schemes are applied. In this paper, we propose an FPGA-based fault injection framework which is able to identify the most critical registers of an entire microprocessor. Further-more, our framework identifies critical variables in the source code of an arbitrary application running in its native environment. We verify the feasibility and relevance of our approach by implementing a lightweight and efficient error correction mechanism protecting only the most critical parts of the system. Experimental results with state estimation applications demonstrate a significantly reduced number of critical calculation errors caused by faults injected into the processor.

An iterative flow to generate test sets providing high fault coverage under extreme parameter variations is presented. The generation is guided by the novel metric of circuit coverage, calculated by massively parallel statistical fault simulation on GPGPUs. Experiments show that the statistical fault coverage of the generated test sets exceeds by far that achieved by standard approaches.

Adequate coverage of small-delay defects in circuits affected by statistical process variations requires identification and sensitization of multiple paths through potential defect sites. Existing K longest path generation (KLPG) algorithms use a data structure called path store to prune the search space by restricting the number of sub-paths considered at the same time. While this restriction speeds up the KLPG process, the algorithms lose their optimality and do not guarantee that the K longest sensitizable paths are indeed found. We investigate, for the first time, the effects of missing some of the longest paths on the defect coverage. We systematically quantify how setting different limits on the path-store size affects the numbers and relative lengths of identified paths, as well as the run-times of the algorithm. We also introduce a new optimal KLPG algorithm that works iteratively and pinpointedly addresses defect locations for which the path-store size limit has been exceeded in previous iterations. We compare this algorithm with a naïve KLPG approach that achieves optimality by setting the path-store size limit to a very large value. Extensive experiments are reported for 45nm-technology data.

SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate. In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing.

Power droop is a non-trivial signal-integrity-related effect triggered by specific power-supply conditions. High-frequency and low-frequency power droop may lead to failure of an IC during application time, but they usually remain undetected by state-of-the-art manufacturing test methods, as the fault excitation imposes particular conditions on global switching activity over several time frames. Hence, ATPG for power-droop test (PD-ATPG) is an extremely hard problem that has not yet been solved optimally. In this paper, we use a SAT-based ATPG engine that employs a mechanism known as SAT-solving with qualitative preferences to generate a solution guaranteed to be optimal for a given set of optimisation criteria, however at the expense of high SAT-solving times. Therefore, a well-balanced set of criteria has to be chosen for the SAT-formulation in order to get as good solutions as possible without rendering the SAT-instances impracticably hard. We explore several strategies and evaluate them experimentally.

Fault simulation is an essential tool in electronic design automation. The accuracy of the computation of fault coverage in classic n-valued simulation algorithms is compromised by unknown (X) values. This results in a pessimistic underestimation of the coverage, and overestimation of unknown (X) values at the primary and pseudo-primary outputs. This work proposes the first stuck-at fault simulation algorithm free of any simulation pessimism in presence of unknowns. The SAT-based algorithm exactly classifies any fault and distinguishes between definite and possible detects. The pessimism w.r.t. unknowns present in classic algorithms is discussed in the experimental results on ISCAS benchmark and industrial circuits. The applicability of our algorithm to large industrial circuits is demonstrated.

Post-silicon validation, i.e., physical characterization of a small number of fabricated circuit instances before start of high-volume manufacturing, has become an essential step in integrated circuit production. Post-silicon validation is required to identify intricate logic or electrical bugs which could not be found during pre-silicon verification. In addition, physical characterization is useful to determine the performance distribution of the manufactured circuit instances and to derive performance yield. Test vectors used for this step are subject to different requirements compared to vectors for simulation-based verification or for manufacturing test. In particular, they must sensitize a very comprehensive set of paths in the circuit, assuming massive variations and possible modeling deficiencies. An inadequate test vector set may result in overly optimistic yield estimates and wrong manufacturing decisions. On the other hand, the size of the test vector set is less important than in verification or manufacturing test. In this paper, we systematically investigate the relationship between the quality of the employed test vectors and the accuracy of yield-performance predictions. We use a highly efficient SAT-based algorithm to generate comprehensive test vector sets based on simple model assumptions and validate these test sets using simulated circuit instances which incorporate effects of process variations. The obtained vector sets can also serve as a basis for adaptive manufacturing test.

The detection of small-delay faults is traditionally performed by sensitizing transitions on a path of sufficient length from an input to an output of the circuit going through the fault site. While this approach allows efficient test generation algorithms, it may result in false positives and false negatives as well, i.e. undetected faults are classified as detected or detectable faults are classified as undetectable. We present an automatic test pattern generation algorithm which considers waveforms and their propagation on each relevant line of the circuit. The model incorporates individual delays for each gate and filtering of small glitches. The algorithm is based on an optimized encoding of the test generation problem by a Boolean satisfiability (SAT) instance and is implemented in the tool WaveSAT. Experimental results for ISCAS-85, ITC-99 and industrial circuits show that no known definition of path sensitization can eliminate false positives and false negatives at the same time, thus resulting in inadequate small-delay fault detection. WaveSAT generates a test if the fault is testable and is also capable of automatically generating a formal redundancy proof for undetectable small-delay faults; to the best of our knowledge this is the first such algorithm that is both scalable and complete.

We present SATSEQ, a timing-aware ATPG system for small-delay faults in non-scan circuits. The tool identifies the longest paths suitable for functional fault propagation and generates the shortest possible sub-sequences per fault. Based on advanced model-checking techniques, SATSEQ provides detection of small-delay faults through the longest functional paths. All test sequences start at the circuit's initial state; therefore, overtesting is avoided. Moreover, potential invalidation of the fault detection is taken into account. Experimental results show high detection and better performance than scan testing in terms of test application time and overtesting-avoidance.

Failures caused by phenomena such as crosstalk or power-supply noise are gaining in importance in advanced nanoscale technologies. The detection of such complex defects benefits from the satisfaction of certain constraints, for instance justifying specific transitions on neighbouring lines of the defect location. We present a SAT-based ATPG-tool that supports the enhanced conditional multiple-stuck-at fault model (ECMS@). This model can specify multiple fault locations along with a set of hard conditions imposed on arbitrary lines; hard conditions must hold in order for the fault effect to become active. Additionally, optimisation constraints that may be required for best coverage can be specified via a set of soft conditions. The introduced tool justifies as many of these conditions as possible, using a mechanism known as SAT with preferences. Several applications are discussed and evaluated by extensive experimental data. Furthermore, a novel fault-clustering technique is introduced, thanks to which the time required to classify all stuck-at faults in a suite of industrial benchmarks was reduced by up to 65%.

Recently a new method called ATE assisted compaction for achieving test response compaction has been proposed. The method relies on testers to achieve additional compaction, without compromising fault coverage, beyond what may already be achieved using on-chip response compactors. The method does not add additional logic or modify the circuit under test or require additional tests and thus can be used with any design including legacy designs. In this work, we enhance this method so that the level of diagnostic resolution achieved without it can be maintained. Experimental results on larger ISCAS-89 show that additional test response compaction can be achieved while diagnostic resolution for single and double stuck-at faults is not adversely impacted by the procedure.

We present a versatile method that enumerates all or a user-specified number of longest sensitisable paths in the whole circuit or through specific components. The path information can be used for design and test of circuits affected by statistical process variations. The algorithm encodes all aspects of the path search as an instance of the Boolean Satisfiability Problem (SAT), which allows the method not only to benefit from recent advances in SAT-solving technology, but also to avoid some of the drawbacks of previous structural approaches. Experimental results for academic and industrial benchmark circuits demonstrate the method's accuracy and scalability.

3D IC technology has demonstrated significant performance and power gains over 2D. However, for technology to be viable yield should be increased. Testing a complete 3D IC after stacking leads to an exponential decay in yield. Pre-bond tests are required to insure correct functionality of the die. In this work we propose a hypergraph based biased netlist partitioning scheme scheme for pre-bond testing of individual dies to reduce extra-hardware (flip-flops) required. Further reduction in hardware is achieved by a logic cone based flip-flop sharing scheme. Simulation results on ISCAS89 benchmark circuits and several industrial benchmarks demonstrate the effectiveness of the proposed approach.

In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i.e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.

Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance in the analysis of safety-critical systems, e.g., in the automotive context. Satisfiability results of a solver can usually be checked by probing the computed solution. This is in general not the case for un-satisfiability results. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-linear arithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete/continuous systems. Furthermore, we test our approach by enhancing the iSAT constraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing the effectiveness of our techniques are given.

Manufacturing defects in nanoscale technologies have highly complex timing behaviour that is also affected by process variations. While conventional wisdom suggests that it is optimal to detect a delay defect through the longest sensitisable path, non-trivial defect behaviour along with modelling inaccuracies necessitate consideration of paths of well-controlled length during test generation. We present a generic methodology that yields tests through all sensitisable paths of user-specified length. The resulting tests can be employed within the framework of adaptive testing. The methodology is based on encoding the problem as a Boolean-satisfiability (SAT) instance and thereby leverages recent advances in SAT-solving technology.

Nanoelectronic circuits are increasingly affected by massive statistical process variations, leading to a paradigm shift in both design and test area. In circuit and system design, a broad class of methods for robustness like statistical design and self calibration has emerged and is increasingly used by the industry. The test community's answer to the massive-variation challenge is currently adaptive test. The test stimuli are modified on the fly (during test application) based on the circuit responses observed. The collected circuit outputs undergo statistical post-processing to facilitate pass/fail classification. We will present fundamentals of adaptive and robust test techniques and their theoretical background. While adaptive test is effective, the understanding how it covers defects under different process parameter combinations is not fully established yet with respect to algorithmic foundations. For this reason, novel analytic and algorithmic approaches in the field of variation-aware testing will also be presented in the tutorial. Coverage of defects in the process parameter space is modeled and maximized by an interplay between special fault simulation and multi-constrained ATPG algorithms. These systematic approaches can complement adaptive test application schemes to form a closed-loop system that combines analytical data with measurement results for maximal test quality.

Nanoscale integrated circuits suffer both from high defect densities and increased parameter variations possibly affecting the overall timing behaviour. Components with a higher vulnerability to process variations are not just critical during test design and test application, but also during normal operation. In particular, ageing effects and changes in the operation environment including supply voltage, temperature and radiation, can easily aggravate the effects of parameter variations inherent to the manufacturing process. Online and offline techniques that attempt to cope with such effects, like online error detection and correction, online diagnosis and hardening, have high cost and therefore cannot be applied to the whole circuit. Making a good selection of components to apply these techniques to, requires accurate metrics for gate criticality under process variations. This paper presents a SAT-based approach to measure criticality. The algorithm requires a minimal amount of physical and electrical data, but it delivers a very good criticality estimate in a fraction of the time required by accurate statistical simulation. The results are validated by comparison to an exact simulation-based approach.

State-of-the-art cyber-physical systems are increasingly deployed in harsh environments with non-negligible soft error rates, such as aviation or search-and-rescue missions. State-of-the-art nanoscale manufacturing technologies are more vulnerable to soft errors. In this paper, we present an FPGA-based framework for injecting soft errors into user-specified memory elements of an entire microprocessor (MIPS32) running application software. While the framework is applicable to arbitrary software, we demonstrate its usage by characterizing soft errors effects on several software filters used in aviation for probabilistic sensor data fusion.

Assume we have a network of discrete-time Markov decision processes (MDPs) which synchronize via common actions. We investigate how to compute probability measures in case the structure of some of the component MDPs (so-called blackbox MDPs) is not known. We then extend this computation to work on networks of MDPs that share integer data variables of finite domain. We use a protocol which spreads information within a network as a case study to show the feasibility and effectiveness of our approach.

In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relev

Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

Transient or soft errors caused by various environmental effects are a growing concern in micro and nanoelectronics. We present a general framework for modeling and mitigating the logical effects of such errors in digital circuits. We observe that some errors have time-bounded effects; the system's output is corrupted for a few clock cycles, after which it recovers automatically. Since such erroneous behavior can be tolerated by some applications, i.e., it is noncritical at the system level, we define the critical soft error rate (CSER) as a more realistic alternative to the conventional SER measure. A simplified technology-independent fault model, the single transient fault (STF), is proposed for efficiently estimating the error probabilities associated with individual nodes in both combinational and sequential logic. STFs can be used to compute various other useful metrics for the faults and errors of interest, and the required computations can leverage the large body of existing methods and tools designed for (permanent) stuck-at faults. As an application of the proposed methodology, we introduce a systematic strategy for hardening logic circuits against transient faults. The goal is to achieve a desired level of CSER at minimum cost by selecting a subset of nodes for hardening against STFs. Exact and approximate algorithms to solve the node selection problem are presented. The effectiveness of this approach is demonstrated by experiments with the ISCAS-85 and -89 benchmark suites, as well as some large (multimillion-gate) industrial circuits.

To achieve a high product quality for nano-scale systems both realistic defect mechanisms and process variations must be taken into account. While existing approaches for variation-aware digital testing either restrict themselves to special classes of defects or assume given probability distributions to model variabilities, the proposed approach combines defect-oriented testing with statistical library characterization. It uses Monte Carlo simu-lations at electrical level to extract delay distributions of cells in the presence of defects and for the defect-free case. This allows distinguishing the effects of process variations on the cell delay from defect-induced cell delays under process variations. To provide a suitable interface for test algorithms at higher levels of abstraction the distributions are represented as histograms and stored in a histogram data base (HDB). Thus, the computationally expensive defect analysis needs to be performed only once as a preprocessing step for library characterization, and statistical test algorithms do not require any low level information beyond the HDB. The generation of the HDB is demonstrated for primitive cells in 45nm technology.

SAT-based automatic test pattern generation has several advantages compared to conventional structural procedures, yet often yields too large test sets. We present a dynamic compaction procedure for SAT-based ATPG which utilizes internal data structures of the SAT solver to extract essential fault detection conditions and to generate patterns which cover multiple faults. We complement this technique by a state-of-the-art forward-looking reverse-order simulation procedure. Experimental results obtained for an industrial benchmark circuit suite show that the new method outperforms earlier static approaches by approximately 23%.

A significant increase in power density in modern nano-electronic VLSI circuits has lead to increased localized heating and generation of hot spots. These temperature effects can lead to reliability and performance problems. This paper presents a novel design time temperature aware methodology which consists of using additional routing known as Heat Pipes, to transfer heat from hot to cold regions. In order to evaluate the effect of Heat Pipes, a thermal model to simulate effect of metal interconnect on heat distribution is also developed. Results show a 5% to 7% decrease in temperature variation through-out and 2 to 3 degree reduction in hotspot temperature as a result of Heat Pipes.

Robust circuit design has become a major concern for nanoscale technologies. As a consequence, for design validation, not only the functionality of a circuit has to be considered, but also its robustness properties have to be analyzed. In this work we propose a method to verify the strong fault-secureness by use of constrained SAT-based ATPG. Strongly fault-secure circuits can be seen as the widest class of circuits achieving the totally self-checking (TSC) goal, which requires that every fault be detected the first time it manifests itself as an error at the outputs. As the strongly fault-secure property guarantees to achieve the TSC goal even in the case of fault accumulation, the effects of all possible fault sequences have to be taken into consideration to verify this property. To speed up the complex analysis of multiple faults we develop rules to derive detectability or redundancy information for multiple faults from the respective information for single faults. For the case of not strongly fault-secure circuits our method provides measures to grade the ldquoextentrdquo of strong fault-secureness given by the implementation.

In this paper a new electrical model is proposed to be used in fault size based fault simulation of crosstalk aggravated resistive short defects. The electrical behavior of the defect is first described and analyzed in details. Then an electrical model is proposed allowing to efficiently compute the critical resistance determining the range of detectable short resistance. The model is validated by comparison with SPICE simulations.

A high-performance resistive bridging fault simulator SUPERB (Simulator Utilizing Parallel Evaluation of Resistive Bridges) is proposed. It is based on fault sectioning in combination with parallel-pattern or parallel-fault multiple-stuck-at simulation. It outperforms a conventional interval-based resistive bridging fault simulator by three orders of magnitude while delivering identical results. Further competing tools are outperformed by several orders of magnitude. Industrial-size circuits, including a multi-million-gates design, could be simulated with runtimes within an order of magnitude of the runtimes for pattern-parallel stuck-at fault simulation.

Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like Statemate support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of Statemate enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.

We report the successful application of a resistive bridging fault (RBF) simulator to industrial benchmark circuits. Despite the slowdown due to the consideration of the sophisticated RBF model, the run times of the simulator were within an order of magnitude of the run times for pattern-parallel complete-circuit stuck-at fault simulation. Industrial-size circuits, including a multi-million-gates design, could be simulated in reasonable time despite a significantly higher number of faults to be simulated compared with stuck-at fault simulation.

Many classes of applications are inherently tolerant to errors. One such class are applications designed for a human end user, where the capabilities of the human cognitive system (cognitive resilience) may compensate some of the errors produced by the application. We present a methodology to automatically distinguish between tolerable errors in imaging applications which can be handled by the human cognitive system and severe errors which are perceptible to a human end user. We also introduce an approach to identify non-critical spots in a hardware circuit which should not be hardened against soft errors because errors that occur on these spots are tolerable. We demonstrate that over 50% of flip-flops in a JPEG compressor chip are non-critical and require no hardening.

We present a simulator which determines the coverage of small-delay faults, i.e., delay faults with a size below one clock cycle, caused by resistive-open defects. These defects are likely to escape detection by stuck-at or transition fault patterns. For the first time, we couple the calculation of the critical size of a small-delay fault with the computation of the resistance range of the corresponding resistive-open defect for which this size is exceeded. By doing so, we are able to extend probabilistic fault coverage metrics initially developed for static resistive bridging faults to small-delay defects.

Hardening a circuit against soft errors should be performed in early design steps before the circuit is laid out. A viable approach to achieve soft error rate (SER) reduction at a reasonable cost is to harden only parts of a circuit. When selecting which locations in the circuit to harden, priority should be given to critical spots for which an error is likely to cause a system malfunction. The criticality of the spots depends on parameters not all available in early design steps. We employ a selection strategy which takes only gate-level information into account and does not use any low-level electrical or timing information. We validate the quality of the solution using an accurate SER estimator based on the new UGC particle strike model. Although only partial information is utilized for hardening, the exact validation shows that the susceptibility of a circuit to soft errors is reduced significantly. The results of the hardening strategy presented are also superior to known purely topological strategies in terms of both hardware overhead and protection.

Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w. r. t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210% and a speed-up of the CPU runtime up to 390% compared to the relation-oriented approach are achieved. But there are also relevant examples, e. g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300% in terms of CPU-time, showing that both approaches are efficient for different scenarios.

We present a flow to extract, simulate and generate test patterns for interconnect open defects. In contrast to previous work, the accuracy of defect modeling is improved by taking the thresholds of logic gates as well as noise margins into account. Efficient fault simulation is enabled by employing an aggressive fault collapsing strategy and an optimized fault list ordering heuristic which allows to combine the advantages of event-driven simulation with bit parallelism. Test generation complexity is kept in check by generating patterns for technology-independent segment-stuck-at faults first, thus reducing (though not completely eliminating) the need for sophisticated technology-aware test generation. Moreover, a comprehensive untestability analysis identifies new classes of untestable faults. Experimental results demonstrate high efficiency of the new flow, outperforming earlier work by two orders of magnitude.

We present a fully automated flow to generate test patterns for interconnect open defects. Both inter-layer opens (open- via defects) and arbitrary intra-layer opens can be targeted. An aggressor-victim model used in industry is employed to describe the electrical behavior of the open defect. The flow is implemented using standard commercial tools for parameter extraction (PEX) and test generation (ATPG). A highly optimized branch-and bound algorithm to determine the values to be assigned to the aggressor lines is used to reduce both the ATPG efforts and the number of aborts. The resulting test sets are smaller and achieve a higher defect coverage than stuck-at n-detection test sets, and are robust against process variations.

Test application at reduced power supply voltage (low-voltage testing) or reduced temperature (low-temperature testing) can improve the defect coverage of a test set, particularly of resistive short defects. Using a probabilistic model of two-line nonfeedback short defects, we quantify the coverage impact of low-voltage and low-temperature testing for different voltages and temperatures. Effects of statistical process variations are not considered in the model. When quantifying the coverage increase, we differentiate between defects missed by the test set at nominal conditions and undetectable defects (flaws) detected at non nominal conditions. In our analysis, the performance degradation of the device caused by lower power supply voltage is accounted for. Furthermore, we describe a situation in which defects detected by conventional testing are missed by low-voltage testing and quantify the resulting coverage loss. Experimental results suggest that test quality is improved even if no cost increase is allowed. If multiple test applications are acceptable, a combination of low voltage and low temperature turns out to provide the best coverage of both hard defects and flaws.

This paper describes the multithreaded MiraXT SAT solver which was designed to take advantage of current and future shared memory multiprocessor systems. The paper highlights design and implementation details that allow the multiple threads to run and cooperate efficiently. Results show that in single threaded mode, MiraXT compares well to other state of the art solvers on industrial problems. In threaded mode, it provides cutting edge performance, as speedup is obtained on both SAT and UNSAT instances.

A high-performance resistive bridging fault simulator SUPERB (Simulator Utilizing Parallel Evaluation of Resis- tive Bridges) is proposed. It is based on fault sectioning in combination with parallel-pattern or parallel-fault multiple- stuck-at simulation. It outperforms a conventional interval- based resistive bridging fault simulator by 60X to 120X while delivering identical results. Further competing tools are out- performed by several orders of magnitude.

Open-via defects are a major systematic failure mechanism in nanoscale manufacturing processes. We present a flow for simulating open-via defects. Electrical parameters are extracted from the layout and technology data and represented in a way which allows efficient simulation on gate level. The simulator takes oscillation caused by open-via defects into account and quantifies its impact on defect coverage. The flow can be employed for manufacturing test as well as for defect diagnosis.

In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of theproblem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.

Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept ofBlack Boxes- parts of the design with unknown behavior - to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of 'uniform counterexamples' to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.

Practical on-line test methods do not cover all possible faults of a system. We propose a method to identify critical faults and distinguish them from non-critical ones. Low-cost on-line fault detection can focus on the critical faults. Alternatively, the circuit sites associated with critical faults could be selectively hardened to improve the overall reliability of a system. This is done in a cost-effective way because no hardening against non-critical faults is required. In this work, we concentrate on faults in imaging applications such as video. We classify faults based on their impact on the system behavior, i.e., the visibility of their effects by a human end-user. The psychovisual model from the JPEG compression method is used for fault effect classification.

Transient or soft errors are an increasing problem in mainstream microelectronics. We propose a framework for modeling transient-error tolerance (TET) in logic circuits. We classify transient errors as critical or non-critical according to their impact on circuit behavior, such as their ability to disturb the internal state for specified periods of time. We introduce a metric called the critical soft-error rate (CSER) as an alternative to conventional SER, and present some analysis strategies based on CSER. This approach employs a new single transient fault (STF) model, which is defined in terms of a temporary stuck-at fault and its associated circuit state. Although basically technology-independent, STFs can be extended with low-level physical attributes. With STFs, we can estimate the transient error probability perrof a circuit's nodes, as well as various measures of error susceptibility and TET. We demonstrate the use of STFs with combinational and sequential circuits, including several types of adders. We also present a systematic hardening strategy that uses perras a guide to improving TET.

This paper addresses the efficiency of IDDQand more specifically Delta- IDDQtesting when using a realistic short defect model that properly considers the relation between the resistance of the short and its detectability. The results clearly show that the Delta-IDDQapproach covers a large number of resistive shorts missed by conventional logic testing, requiring only a relatively small vector set. In addition a significant number of defects which are proven to be undetectable by logic testing but may deteriorate and result in reliability failures are detected. The Delta- IDDQthreshold and thus the equipment sensitivity is shown to be critical for the test quality. Furthermore, the validity of the traditional IDDQfault models when considering resistive short defects is found to be limited. For instance, the use of the fault-free next-state function for sequential IDDQfault simulation is shown to result in a wrong classification of some resistive short defects. This is the first systematic study of IDDQtesting of resistive short defects. The impact of the threshold on the defect coverage is quantified for the first time. Although the simulation results are based upon a 0.35mum technology, the results and methodology can be transferred to state-of-the-art and NanoTechnologies

This paper analyzes the electrical behaviour of resistive opens as a function of their unpredictable resistance. It is demonstrated that the electrical behaviour depends on the value of the open resistance. It is also shown that detection of the open by a given vector Tirecursively depends on all the vectors that have been applied to the circuit before Ti. An electrical analysis of this recursive effect is presented and a specific ATPG strategy is proposed

Circuit activity is a function of input patterns. When circuit activity changes abruptly, it can cause sudden drop or rise in power supply voltage. This change is known as power droop and is an instance of power supply noise. Although power droop may cause an IC to fail, such failures cannot currently be screened during testing as it is not covered by conventional fault models. In this paper we present a technique for screening such failures. We propose a heuristic method to generate test sequences which create worst-case power drop by accumulating the high-frequency and low-frequency effects. The generated patterns need to be sequential even for scan designs. We employ a dynamically constrained version of the classical D-algorithm for test generation, i.e., the algorithm generates new constraints on-the-fly depending on previous assignments. The obtained patterns can be used for manufacturing testing as well as for early silicon validation. A prototype ATPG is implemented to demonstrate the feasibility of the approach and test sequences are generated for ISCAS circuits.

The authors present a simulator for resistive-bridging and stuck-at faults. In contrast to earlier work, it is based on electrical equations rather than table look up, thus, exposing more flexibility. For the first time, simulation of sequential circuits is dealt with; interaction of fault effects in current time frame and earlier time frames is elaborated on for different bridge resistances. Experimental results are given for resistive-bridging and stuck-at faults in combinational and sequential circuits. Different definitions of fault coverage are listed, and quantitative results with respect to all these definitions are given for the first time.

We present a technique for making a circuit ready for logic built-in self test by masking unknown values at its outputs. In order to keep the silicon area cost low, some known bits in output responses are also allowed to be masked. These bits are selected based on a stuck-at n-detection based metric, such that the impact of masking on the defect coverage is minimal. An analysis based on a probabilistic model for resistive short defects indicates that the coverage loss for unmodeled defects is negligible for relatively low values of n.

Resistive defects are gaining importance in very-deepsubmicron technologies, but their detection conditions are not trivial. Test application can be performed under reduced temperature and/or voltage in order to improve detection of these defects. This is the first analytical study of resistive bridge defect coverage of CMOS ICs under low-temperature and mixed low-temperature, low-voltage conditions. We extend a resistive bridging fault model in order to account for temperature-induced changes in detection conditions. We account for changes in both the parameters of transistors involved in the bridge and the resistance of the short defect itself. Using a resistive bridging fault simulator, we determine fault coverage for low-temperature testing and compare it to the numbers obtained at nominal conditions. We also quantify the coverage of flaws, i.e. defects that are redundant at nominal conditions but could deteriorate and become earlylife failures. Finally, we compare our results to the case of low-voltage testing and comment on combination of these two techniques.

Reversibility is of interest in achieving extremely low power dissipation; it is also an inherent design requirement of quantum computation. Logical fault models for conventional circuits such as stuck-at models are not wellsuited to quantum circuits. We derive a family of logical fault models for reversible circuits composed of k- CNOT (k-input controlled-NOT) gates and implementable by many technologies. The models are extensions of the previously proposed single missing-gate fault (MGF) model, and include multiple and partial MGFs. We study the basic detection requirements of the new fault types and derive bounds on the size of their test sets. We also present optimal test sets computed via integer linear programming for various benchmark circuits. These results indicate that, although the test sets are generally very small, partial MGFs may need significantly larger test sets than single MGFs.

Test data compression has become increasingly popular for distributing test complexity between automatic test equipment and on-chip structures. We provide a general formulation for the code-based test compression problem with fixed-length input blocks and propose a solution approach based on evolutionary algorithms. In contrast to existing code-based methods, we allow unspecified values in matching vectors, which allows encoding of arbitrary test sets using a relatively small number of codewords. Experimental results for both stuck-at and path delay fault test sets for ISCAS circuits demonstrate an improvement compared to existing techniques.

A unified gate-level fault model for interconnect opens and bridges is proposed. Defects are modeled as constrained multiple line stuck-at faults. A novel feature of the proposed fault model is its flexibility to accommodate increasing levels of accuracy. Additionally the model does not require accurate device level circuit models to achieve desired accuracy. Efficient methods for fault simulation and test generation are discussed and experimental results on benchmark circuits and industrial designs are presented. The experimental results presented show that the tests generated using simpler versions of the proposed fault model achieve higher defect coverage than the tests using two currently popular methods to derive high defect coverage tests.

Technology trends are increasing the frequency of serious transient (soft) faults in digital systems. For example, ICs are becoming more susceptible to cosmic radiation, and are being embedded in applications with dynamic noisy environments. We propose a generic framework for representing such faults and characterizing them on-line. We formally define the impact of a transient fault in terms of three basic parameters: frequency, observability and severity. We distinguish fault modes in systems whose noise environment changes dynamically. Based on these ideas, the problem of designing on-line architectures for transient fault characterization is formulated and analyzed for several optimization goals. Finally, experiments are described that determine transient fault impact and the corresponding tests for various simulated fault modes of the ISCAS-89 benchmark circuits.

We present three resistive bridging fault models valid for different CMOS technologies. The models are partitioned into a general framework (which is shared by all three models) and a technology-specific part. The first model is based on Shockley equations and is valid for conventional but not deep submicron CMOS. The second model is obtained by fitting SPICE data. The third resistive bridging fault model uses Berkeley predictive technology model and BSIM4; it is valid for CMOS technologies with feature sizes of 90nm and below, accurately describing non-trivial electrical behavior in that technologies. Experimental results for ISCAS circuits show that the test patterns obtained for the Shockley model are still valid for the fitted model, but lead to coverage loss under the predictive model.

Logical reversibility occurs in low-power applications and is an essential feature of quantum circuits. Of special interest are reversible circuits constructed from a class of reversible elements called k-CNOT (controllable NOT) gates. We review the characteristics of k-CNOT circuits and observe that traditional fault models like the stuck-at model may not accurately represent their faulty behavior or test requirements. A new fault model, the missing gate fault (MGF) model, is proposed to better represent the physical failure modes of quantum technologies. It is shown that MGFs are highly testable, and that all MGFs in an N-gate k-CNOT circuit can be detected with from one to [N/2] test vectors. A design-for-test (DFT) method to make an arbitrary circuit fully testable for MGFs using a single test vector is described. Finally, we present simulation results to determine (near) optimal test sets and DFT configurations for some benchmark circuits.

An ATPG for resistive bridging faults is proposed that combines the advantages of section-based generation and interval-based simulation. In contrast to the solutions introduced so far, it can handle arbitrary non-feedback bridges between two nodes, including ones detectable at higher bridge resistance and undetectable at lower resistance, and faults requiring more than one vector for detection.

Article Orthogonal hypergraph routing for improved visibility Share on Authors: Thomas Eschbach Albert-Ludwigs-University, Freiburg, Germany Albert-Ludwigs-University, Freiburg, GermanyView Profile , Wolfgang Günther Infineon AG CL DAT DF V, Munich, Germany Infineon AG CL DAT DF V, Munich, GermanyView Profile , Bernd Becker Albert-Ludwigs-University, Freiburg, Germany Albert-Ludwigs-University, Freiburg, GermanyView Profile Authors Info & Claims GLSVLSI '04: Proceedings of the 14th ACM Great Lakes symposium on VLSIApril 2004 Pages 385–388https://doi.org/10.1145/988952.989045Published:26 April 2004 2citation212DownloadsMetricsTotal Citations2Total Downloads212Last 12 Months2Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We present a technique for making a circuit ready for logic BIST by masking unknown values at its outputs. In order to keep the silicon area cost low, some known bits in output responses are also allowed to be masked. These bits are selected based on a stuck-at n-detection based metric, such that the impact of masking on the defect coverage is minimal. An analysis based on a probabilistic model for resistive short defects indicates that the coverage loss for unmodeled defects is negligible for relatively low values of n.

Test application at reduced power supply voltage (or VLV testing) is a cost-effective way to increase the defect coverage of a test set. Resistive short defects are a major contributor to this coverage increase. Using a probabilistic model of these defects, we quantify the coverage impact of VLV testing for different voltages. When considering the coverage increase, we differentiate between defects missed by the test set at nominal voltage and undetectable defects (flaws) detected by VLV testing. In our analysis, the performance degradation of the device caused by lower power supply voltage is accounted for. Furthermore, we describe a situation in which defects detected by conventional testing are missed by VLV testing and quantify the resulting coverage loss. We report the numbers on the increased defect coverage, flaw coverage, and coverage loss for ISCAS circuits.

We present a simulator for resistive bridging and stuck-at faults. In contrast to earlier work, it is based on electrical equations rather than table look-up, thus exposing more flexibility. For the first time, simulation of sequential circuits is dealt with; reciprocal action of fault effects in current time frame and earlier time frames is elaborated on for different bridge resistances. Experimental results are given for resistive bridging and stuck-at faults in combinational and sequential circuits. Different definitions of fault coverage are listed and quantitative results with respect to all these definitions are given for the first time.

The layout problem in VLSI-design can be broken up into the subtasks partitioning, floorplanning, placement, and routing. In the routing phase, a large number of connections between the blocks and cells have to be established, while intersections lead to short circuits and, therefore, have to be avoided. We present an approach for exact routing of multiterminal nets that complements traditional routing techniques. It is particularly well suited for an application to dense problem instances and the completion of routing in subregions, which turn out to be difficult for routing tools based on heuristic methods. The exact router proposed uses symbolic methods, i.e., MDDs (multivalued decision diagrams) for representation of the routing space. For the necessary computations of routing solutions, we profit considerably from the efficient basic operations on MDDs. All possible solutions to the routing problem are represented by one single MDD and, once this MDD is given, routability can be decided within constant time. To reduce the search space of possible routing solutions, so-called forced cells are computed. Experimental results are given to show the feasibility and the practicability of the approach.

n-detection test sets for stuck-at faults have been shown to be useful in detecting unmodeled defects. It was also shown that a set of faults, called maximally dominating faults, can play an important role in controlling the increase in the size of an n-detection test set as n is increased. In an earlier work, a superset of the maximally dominating fault set was used. In this work, we propose a method to determine exact sets of maximally dominating faults. We also define a new type of n-detection test sets based on the exact set of maximally dominating faults. We present experimental results to demonstrate the usefulness of this exact set in producing high-quality n-detection test sets.

We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS-Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented.

The computation of the set of reachable states is the key problem of many applications in sequential verification. Binary Decision Diagrams (BDDs) are extensively used in this domain, but tend to blow up for larger instances. To increase the computational power of BDDs, linearly transformed BDDS (LTBDDs) have been proposed. In this paper we show how this concept can be incorporated into the sequential verification domain by restricting dynamic reordering in a way that the relational product can still be carried out efficiently. Experimental results are given to show the efficiency of our approach.

Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [17, 7]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this Multiple Variable Order problem. Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques.

Verification of designs containing pre-designed cores is a challenging topic in modern IC design. Traditional approaches generally do not use the information that parts of the design (like IP cores) are already verified. In this case, the verification of the IP core reduces to verifying the connectivity between the surrounding design and the core. Therefore, we propose a method that is based on test patterns. Using only those patterns for simulation, in almost all cases 100% of the errors can be detected. Existing test access logic is employed for the application of the patterns. A large set of experimental results is given to demonstrate the efficiency of the approach.

We consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification.

In various areas of computer science and mathematics, including scientific computing, task scheduling and VLSI design, the graph concept is used for modeling purposes, and graph partitioning algorithms are required to obtain solutions. For example, with increasing complexities of circuit design the circuit graphs may have several millions of nodes, while the CAD tools, like e.g. layout or visualization tools, work best on smaller subproblems. Thus, often partitions with a large number of components have to be determined. We present GREEDY IIP, a partitioning algorithm based on a sequence of greedy local operations. These operations are combined in an iterative manner directed by a restricted hill climbing approach. The algorithm is particularly successful, if a large number of final partitions, i.e. more than 1000, has to be computed. Experimental results on a large number of benchmarks are given. In comparison to the state-of-the-art tools GREEDY IIP shows significant advantages with respect to quality, space requirements and in many cases also with respect to run time.

Non-standard fault models often require the application of true-pattern testing. A fully-automated approach for generating a multiple scan chain-based architecture is presented so that two-pattern test sets generated for the combinational core can be applied to the sequential circuit. Test time and area overhead constraints are considered.

Symbolic techniques have revolutionized reachability analysis in the last years. Extending their applicability to handle large, industrial designs is a key issue, involving the need to focus on memory consumption for BDD representation as well as time consumption to perform symbolic traversals of Finite State Machines (FSMs). We address the problem of reachability analysis for large FSMs, introducing a novel technique that performs reachability analysis using a sequence of “distance driven” partial traversals based on dynamically chosen prunings of the transition relation. Experiments are given to demonstrate the efficiency and robustness of our approach: We succeed in completing reachability problems with significantly smaller memory requirements and improved time performance.

The introduction of Decision Diagrams (DDs) has brought new means towards solving many of the problems involved in digital circuit design. Compactness of the representation is one key issue. Ordered Pseudo Kronecker Decision Diagrams (OPKDDs) together with the use of complemented edges is known to offer the most general ordered read-once DD representation at the bit-level, hence OPKDDs hold all minimal sized bit-level ordered DDs for a given function. This representation allows us to trade-off diagram canonicity against compactness. Ternary-OPKDDs (TOPKDDs) implicitly holds all OPKDDs for a given variable order. We state the canonicity criteria for TOPKDDs having complemented edges and develop an efficient sifting based method for their minimization. Furthermore, a heuristic minimization algorithm for OPKDDs is devised, utilizing the redundancies of Ternary-OPKDDs (TOPKDDs). Experiments on a set of MCNC benchmarks confirm the potential compactness of OPKDDs and demonstrate the efficiency of the proposed heuristics.

We present an approach for exact switchbox routing that complements traditional routing techniques. It is particularly well suited for an application to dense problem instances and the completion of routing in subregions which turn out to be difficult for routing tools based on heuristic methods. The exact router proposed used symbolic methods i.e. MDDs (Multi-valued Decision Diagrams) for representation of the routing space. All possible solutions to the routing problem are represented by one single MDD and once this MDD is given, routability can be decided within constraint time. To reduce the search space of possible routing solutions, so-called forced cells are computed. Finally, experimental results are given. They show the feasibility and the practicability of the approach.

A symbolic fault simulator is integrated in a Genetic Algorithm (GA) environment to perform Automatic Test Pattern Generation (ATPG) for synchronous sequential circuits. In a two phase algorithm, test length and fault coverage as well are optimized. However, there are circuits with bad random testability properties, that are also hard to test using genetically optimized test patterns. Thus, deterministic aspects are included in the GA environment to improve fault coverage. Experiments demonstrate that tests with higher fault coverages and considerably shorter test sequences than in previously presented approaches are obtained.

The design process of digital circuits is often carried out in individual steps, like logic minimization, mapping and routing. This leads to quality loss, e.g. in cases where highly optimized netlists fit badly onto the target architecture. Lattice diagrams have been proposed as one possible solution. They offer a regular two dimensional structure, thus overcoming the routing problem. However elegant, presented methods have only been shown to find practical lattice representations for small functions. We present heuristic synthesis methods for Pseudo-Symmetric Pseudo Kronecker Decision Diagrams (PSP-KDDs) applicable to incompletely specified multiple output functions. The lattice structure maps directly to both ASICs and fine grain FPGAs. Our method (combining logic minimization, mapping and routing) seeks to minimize area and delay by heuristic methods. Experimental results on a set of MCNC benchmarks show superior quality to previous methods and in many cases even optimal depth results for unfolded lattices.

Several types of Decision Diagrams (DDs) have been proposed for the verijcation of Integrated Circuits. Recently word-level DDs libBblDs, *BhfDs, HDDs, K*BhiDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDsand *PHDDsit wasfor thejrst time possible to formally verifi integer multipliers and Joating point multipliers of "signi&ant" bitlengths, respectively.On the other hat~it has been unhewn, whether division, the operation inverse to multiplication, can be efiiently represented by some ppe of word-level DDs.In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer divisiok Thus, neither a clever choice of the variable orderins, the decomposition type or the edse weights, can lead to a polynotnial DD size for divisio~ For the proof we introduce Word-Level Linear Combination Dia-gr~(JVLCDS), a DD, which maybe viewed as a "generic" wordlevel DD. \i@derive an uponential lower bound on the WLCD representation sizefor integer dividers atrdshow how this bound transfers to all other word-level DDs.

We present methods for the construction of small ordered Kronecker Functional Decision Diagrams (OKFDDs). OKFDDs are a generalization of ordered binary decision diagrams (OBDDs) and ordered functional decision diagrams (OFDDs) as well. Starting with an upper bound for the size of an OKFDD representing a tree-like circuit, we develop different heuristics to find good variable orderings and decomposition types for OKFDDs representing two-level and multilevel circuits, respectively. Experimental results are presented to show the efficiency of our approaches.

Ordered Kronecker functional decision diagrams (OKFDD's) are a data structure for efficient representation and manipulation of Boolean functions. OKFDD's are a generalization of ordered binary decision diagrams (OBDD)s) and ordered functional decision diagrams and thus combine the advantages of both. In this paper, basic properties of OKFDD's and their efficient representation and manipulation are given. Starting with elementary manipulation algorithms, we present methods for the construction of small OKFDD's. Our approach is based on dynamic variable ordering and decomposition-type choice. For changing the decomposition type, we use an efficient reordering-based method. We briefly discuss the implementation of PUMA, an OKFDD package, which was used in all our experiments. These experiments demonstrate the quality of our methods in comparison to sifting and interleaving for OBDD's.

Several types of Decision Diagrams (DDs) have have been proposed in the area of Computer Aided Design (CAD), among them being bit-level DDs like OBDDs, OFDDs and OKFDDs. While the aforementioned types of DDs are suitable for representing Boolean functions at the bit-level and have proved useful for a lot of applications in CAD, recently DDs to represent integer-valued functions, like MTBDDs (=ADDs), EVBDDs, FEVBDDs, (*)BMDs, HDDs (=KBMDs), and K*BMDs, attract more and more interest, e.g., using *BMDs it was for the first time possible to verify multipliers of bit length up to n=256. In this paper we clarify the representational power of these DD classes. Several (inclusion) relations and (exponential) gaps between specific classes differing in the availability of additive and/or multiplicative edge weights and in the choice of decomposition types are shown. It turns out for example, that K(*)BMDs, a generalization of OKFDDs to the word-level, also "include" OBDDs, MTBDDs and (*)BMDs. On the other hand, it is demonstrated that a restriction of the K(*)BMD concept to subclasses, such as OBDDs, MTBDDs, (*)BMDs as well, results in families of functions which lose their efficient representation.

Ordered Kronecker Functional Decision Diagrams (OKFDDs) are a data structure for efficient representation and manipulation of Boolean functions. OKFDDs are very sensitive to the chosen variable ordering and the decomposition type list, i.e. the size may vary from linear to exponential. In this paper we present an Evolutionary Algorithm (EA) that learns good heuristics for OKFDD minimization starting from a given set of basic operations. The difference to other previous approaches to OKFDD minimization is that the EA does not solve the problem directly. Rather, it develops strategies for solving the problem. To demonstrate the efficiency of our approach experimental results are given. The newly developed heuristics combine high quality results with reasonable time overhead.

In many verification techniques, fast functional evaluation of a Boolean network is needed. We investigate the idea of using binary decision diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.

Until recently verifying multipliers with formal methods was not feasible, even for small input word sizes. About two years ago, a new data structure, called Multiplicative Binary Moment Diagram (*BMD), was introduced for representing arithmetic functions over Boolean variables. Based on this data structure, methods were proposed by which verification of multipliers with input word sizes of up to 256 bits became feasible. Only experimental data has been provided for these verification methods until now. In this paper we give a formal proof that logic verification using *BMDs is polynomially bounded in both space and time when applied to the class of Wallace-tree like multipliers.

We introduce a two-staged Genetic Algorithm for optimizing weighted random pattern testing in a Built-in-Self-Test (BIST) environment. The first stage includes the OBDD-based optimization of input probabilities with regard to the expected test length. The optimization itself is constrained to discrete weight values which can directly be integrated in a BIST environment. During the second stage, the hardware-design of the actual BIST-structure is optimized. Experimental results are given to demonstrate the quality of our approach.

In this paper, a polynomial time algorithm for the minimization of fixed polarity Reed-Muller expressions (FPRMs) for totally symmetric functions based on ordered functional decision diagrams (OFDDs) is presented. A generalization to partially symmetric functions is investigated. The algorithm has been implemented as the program Sympathy. Experimental results in comparison to previously published methods are given to show the efficiency of the approach.

Decision Diagrams are used in design automation for efficient representation of Boolean functions. It is also possible to directly derive circuits from Decision Diagrams. In this paper we present an approach to synthesize circuits from a very general class of Decision Diagrams, the ordered Kronecker Functional Decision Diagrams. These Decision Diagrams make use of Davio decompositions which are based on exclusive-or operations and therefore allow the use of EXOR gates in the synthesized circuits. We investigate area, depth, and testability of these circuits and compare them to circuit designs generated by other synthesis tools. Experimental results show that the presented approach is suitable to overcome the trade-off between depth and testability at the price of reasonable area overhead.

Local transformations are used in several synthesis approaches. During application of such transformations attention has to be paid to many important properties, e.g. area, speech, power consumption, and testability. In this paper we study relations between local transformations and delay fault testability. In delay testing it is not necessary to test every path in a circuit to ascertain correct timing behavior. For example, a set of robust dependent path delay faults need not be considered for testing if all paths that are not robust dependent are tested. We present sufficient conditions for local transformations which ensure that a test set for all non-robust-dependent paths in the original circuit is also a test set for all non-robust-dependent paths in the transformed circuit. These conditions are applied to some local transformations which are often used in logic synthesis and it is shown that they preserve testability. The impact of local transformations on robust dependent testability is demonstrated by experimental results performed on benchmark circuits.

We present a tool to compute a synchronizing sequence for synchronous sequential circuits. It consists of three parts. One part is an OBDD-based approach combined with a heuristic algorithm for preventing a memory overflow. This approach potentially finds a minimum length reset sequence. The second part is an improved three-valued based greedy algorithm. Its synchronizing sequence is not minimal in all cases, but experiments show that it is actually very good. The third part of the tool (and the focus of this paper) is a routine to quickly decide the non-resetability of a design. In contrast to previous approaches this routine is based on sufficient functional conditions to prove the non-resetability of certain memory elements. For the first time results about the resetability of the largest ISCAS'89 benchmark circuits are presented.

We present methods to minimize fixed polarity Reed-Muller expressions (FPRMs), i.e., two-level fixed polarity AND/EXOR canonical representations of Boolean functions, using ordered functional decision diagrams (OFDDs). We investigate the close relation between both representations and use efficient algorithms on OFDDs for exact and heuristic minimization of FPRMs. In contrast to previously published methods, our algorithm can also handle circuits with several outputs. Experimental results on large benchmarks are given to show the efficiency of our approach.

No abstract available.

Abstract| F ault simulation for synchronous sequential circuits is a very time-consuming task.The complexity of the task increases if there is no information about the initial state of the circuit.In this case an unknown initial state is assumed which is usually handled by i n troducing a three-valued logic.As it is well-known fault simulation based on this logic only determines a lower bound of the fault coverage.Recently it has been shown that fault simulation based on the multiple observation time test strategy can improve the accuracy of the fault coverage.In this paper we describe how this strategy can be successfully implemented based on Ordered Binary Decision Diagrams.Our experiments demonstrate the eciency of the fault simulation procedure developed.

We present methods for the construction of small Ordered Kronecker Functional Decision Diagrams (OKFDDs). OKFDDs are a generalization of Ordered Binary Decision Diagrams (OBDDs) and Ordered Functional Decision Diagrams (OFDDs) as well. Our approach is based on dynamic variable ordering and decomposition type choice. For changing the decomposition type we use a new method. We briefly discuss the implementation of PUMA, our OKFDD package. The quality of our methods in comparison with sifting and interleaving for OBDDs is demonstrated based on experiments performed with PUMA.

Several types of local transformations and their effect on path delay fault testability have been examined in the literature. In this paper we present SALT (System for Application of Local Transformations), which is a general tool for the application of a user-defined set of local transformations. The concepts of "related transformations" and of "pseudo-isomorphism" are introduced, which are used in SALT to allow the application of local transformations more frequently. We use SALT to apply testability preserving and testability improving transformations. The effect of these transformations on the size, depth and testability of the transformed circuits is compared to the results obtained by other approaches on benchmark circuits.

We present a performance driven generator for integer adders which has the following interesting feature: The generator is parametrized in the operands' bitlength n, the delay of the addition t/sub n/, and the fault model FM. FM may in particular be chosen as the classical stuck-at fault model, the cellular fault model or the robust path delay fault model. The output of the generator is a performance oriented conditional sum type adder, i.e., an area-minimal n-bit adder of the "conditional sum type" with delay /spl les/t/sub n/ (if it exists) together with a small complete test set with respect to the chosen fault model FM.>

An efficient package for construction of and operation on ordered Kronecker Functional Decision Diagrams (OKFDD) is presented. OKFDDs are a generalization of OBDDs and OFDDs and as such provide a more compact representation of the functions than either of the two decision diagrams. In this paper basic properties of OKFDDs and their efficient representation and manipulation are presented. Based on the comparison of the three decision diagrams for several benchmark functions, a 25% improve ment in size over OBDDs is observed for OKFDDs.

We present an ordered functional decision diagram (OFDD) based method to minimize fixed polarity Reed-Muller expressions (FPRMs) for very large functions using genetic algorithms (GAs). R. Dreschsler et al. (1994) presented fast heuristic methods for FPRM minimization and compared them to several other approaches. We show that better results for large functions can be obtained if these heuristics are combined with GAs, i.e. we use hybrid GAs (HGAs). Experimental results are given to show the efficiency of the approach.>

Fault simulation for synchronous sequential circuits is a very time-consuming task. The complexity of the task increases if there is no information available about the initial state of the circuit. In this case, an unknown initial state is assumed which is usually handled by introducing a three-valued logic. It is known that fault simulation based upon this logic only determines a lower bound for the fault coverage achieved by a test sequence. Therefore, we developed a hybrid fault simulator H-FS combining the advantages of a fault simulator using the three-valued logic and of an exact symbolic fault simulator based upon binary decision diagrams. H-FS is able to handle even the largest benchmark circuits and thereby determines fault coverages much more accurately than previous algorithms using the three-valued logic.

After a brief review on testability aspects of parallel arithmetical units we focus on n-bit multipliers and especially consider a class of Wallace tree multipliers made suitable for VLSI design by Vuillemin and Luk [VULU].It is shown that for these circuits both optimal running time and optimal test complexity can be obtained.A complete test set according to the single cellular fault model is presented.(In this case, the single cellular fault model is superior to the classical single stuck-at model.)The proposed test only consists of 17 pattern8 for all n.Hence, the multiplier is C-testable, i.e. it can be tested by a number of input combination8 which is independent of the number of cells in the circuit.The extra test hardware is very small.Only two additional ports and n -2 internal connections are necessary.

Considers the design of two well-known optimal time adders: the carry look-ahead adder and the conditional sum adder. It is shown that 6 log/sub 2/(n)-4 and 6 log/sub 2/(n)+2 test patterns suffice to completely test the n-bit carry look-ahead adder and the n-bit conditional sum adder with respect to the single stuck-at fault model (for a given set of basic cells). The results are considered pertinent to establishing the correct behavior of a given VLSI chip.>

We present an algebraic approach to hierarchical design of integrated circuits. This approach is based on a of nets which includes topological as well as behavioural aspects of integrated circuits. We have developed a hierarchical design system called CADIC which is build around this calculus in much the same way as e.g. Algol is build around numerics. An example for the design of a family of fast adders will demonstrate the power of this calculus. Finally we will give a summary outline on the structure of procedures which automatically transform the design into lower design levels.

The optimal planar layout of planar graphs with respect to the $L_1 $- or $L_2 $-metric leads to NP-hard problems, if one assumes the nodes of the graph to be fixed in the plane (see [FiPa], [Be]). In this paper we consider the (optimal) layout of graphs with fixed boundary (i.e., graphs, where only the nodes of a given cycle of the graph have fixed positions in the plane). The investigated layouts are straight line embeddings in a continuous part of the plane; the cost of a layout is calculated with help of very general cost functions including the pth power of the usual Euclidean distance metric for $p = 2,3, \cdots $ (for short, $l_p $-metric). For a large class of graphs, which, for example, occur in chip layout problems as the abstract structure of switching circuits, we show the existence and uniqueness of the optimal layout. The main part of the paper is concerned with planar graphs. We get an interesting characterization of nonplanar layouts of planar graphs, which shows that the optimal layout of a planar graph is planar or at least “quasiplanar.” This property makes it possible to decompose the general layout problem into two independent problems: (i) Find a layout of a circuit that is not necessarily planar, but that has an “lallowed crossing behaviour.” (ii) Fix the crossing points and then optimize the layout. Our theorems show that no new contacts (crossing points) will be generated. In the Appendix we outline some (efficient, polynomial time) methods for the construction of optimal layouts and give as an example the optimal layouts of a recursively defined n-bit adder and multiplier.

The n-cube network is called faulty if it contains any faulty processor or any faulty link. For any number k we are interested in the minimum number f(n, k) of faults, necessary for an adversary to make any (n-k)-dimensional subcube faulty. Reversely formulated: The existence of a (n-k)- dimensional nonfaulty subcube can be guaranteed, unless there are at least f(n,k) faults in the n-cube. In this paper several lower and upper bounds for f(n, k) are derived such that the resulting gaps are "small". For instance if k ≥ 2 is constant, then f(n, k) = θ(log n). Especially for k = 2 and large n: f(n, 2) ∈ [⌈αn⌉ : ⌈αn⌉ + 2] where αn = log n + 1/2 log log n + 1/2. Or if k = ω(log log n) then 2k ≪ f(n, k) ≪ 2(1+ε)k, with ε chosen arbitrarily small. The above upper bounds are obtained by analysing the behaviour of an adversary, who makes "worst-case" distributions of a given number of faulty processors. For k = 2 the distribution is obtained constructively, whereas in the general case only the existence is shown using probabilistic arguments. The above bounds change if the notions are relativized with respect to some given parallel faultchecking procedure P. In this case only those subcubes must be made faulty by the adversary, which are possible outputs of P. In the case k = 2 the notion of directed chromatic index is defined to analyse this situation. Relations between the directed chromatic index and the chromatic number are derived, which are of interest in their own right.