Modern interacting digital systems are becoming increasingly complex, making it difficult to ensure their actual behavior aligns with design-time expectations, particularly in uncertain or dynamic environments, even when specifications are correct. This misalignment affects system scalability, reliability, and increases maintenance costs.We introduce a conceptual framework for identifying and self-explaining mismatches between expected and observed system behavior, together with an algorithm that generates explanations and case studies that apply the conceptual framework for explanation generation in an interacting digital systems setting.

Hybrid systems combine both continuous and discrete behavior. These systems serve as models in many fields, including control systems, robotics, and industrial processes. However, due to their complexity, finding an accurate model is a challenge. This paper presents a holistic approach to learning models of hybrid systems using symbolic regression. Our method leverages symbolic regression to automatically discover accurate and interpretable mathematical models in the form of hybrid systems from observed data. An advantage of our algorithm is that it detects transitions between different behavioral modes of a system based on the inherent dynamics. From learned expressions for the dynamical behavior of a system, we form a hybrid system by combining the learned expressions with a decision tree determining the current behavioral mode from data. This hybrid decision tree serves regression, prediction, and further related tasks. Our results demonstrate that symbolic regression can effectively identify the underlying dynamics of a real hybrid system and predict output signals on new input data with high accuracy. • Hybrid systems are powerful models combining continuous and discrete dynamics. • A data-driven identification automates model generation. • Often, dynamic modes are identified from signal similarities. • Different initial conditions lead to dissimilar signals even for same dynamics. • Dynamics-based identification is a more effective approach.

Specifications for complex designs and their consistency are always a headache. Automated specification mining - including but not limited to generative AI - offers attractive solutions, but there are also various unmet needs.

Identification of hybrid systems requires learning models that capture both discrete transitions and continuous dynamics from observational data. Traditional approaches follow a stepwise process, separating trace segmentation and mode-specific regression, which often leads to inconsistencies due to unmodeled interdependencies. In this paper, we propose a new iterative learning paradigm that jointly optimizes segmentation and flow function identification. The method incrementally constructs a hybrid model by evaluating and expanding candidate flow functions over observed traces, introducing new modes only when existing ones fail to explain the data. The approach is modular and agnostic to the choice of the regression technique, allowing the identification of hybrid systems with varying levels of complexity. Empirical results on benchmark examples demonstrate that the proposed method produces more compact models compared to traditional techniques, while supporting flexible integration of different regression methods. By favoring fewer, more generalizable modes, the resulting models are not only likely to reduce complexity but also simplify diagnostic reasoning, improve fault isolation, and enhance robustness by avoiding overfitting to spurious mode changes.

The IEEE European Test Symposium (ETS) has been facilitating progress in electronic systems testing since its launch in 1996. On the occasion of its 30th anniversary, this collaborative paper gathers sections by 21 ETS teams to outline their influential ideas and milestones. Each team’s section highlights historical perspective, current research, frameworks and projects as well as forward-looking research agendas in the area of electronic-based circuits and systems testing, reliability, safety, security and validation. This anniversary summary documents how research of various ETS teams, exemplifying the test community, has been evolving and transitioning from concepts to practical standards and Electronic Design Automation (EDA) tools and flows. This legacy is a strong base to drive the next generation of advances in electronic systems testing.

Hardware design weaknesses, when overlooked, can lead to security vulnerabilities. Their cost of fixing is higher the later they are found in the development life cycle. The challenges of detecting these issues in the early stages of hardware design, compared to software design, can be attributed to limited research or poorly defined design guidelines. Using the existing hardware design weakness classification by the MITRE Corporation, we evaluated how Information Flow Tracking (IFT) can be utilized to identify security weaknesses in hardware designs. First, we provide a classification of design weaknesses tailored to detection using IFT. Second, we present a case study to identify one of such weaknesses using an open-source IFT tool. Additionally, we discuss the challenges of using IFT to detect information-flow-based hardware design weaknesses.

An increasing number of unhardened commercial-off-the-shelf embedded devices are deployed under harsh operating conditions and in highly-dependable systems. Due to the mechanisms of hardware degradation that affect these devices, ageing detection and monitoring are crucial to prevent critical failures. In this paper, we empirically study the propagation delay of 298 naturally-aged FPGA devices that are deployed in the European XFEL particle accelerator. Based on in-field measurements, we find that operational devices show significantly slower switching frequencies than unused chips, and that increased gamma and neutron radiation doses correlate with increased hardware degradation. Furthermore, we demonstrate the feasibility of developing machine learning models that estimate the switching frequencies of the devices based on historical and environmental data.

Hybrid systems, which combine both continuous and discrete behavior, are used in many fields, including robotics, biological systems, and control systems. However, due to their complexity, finding an accurate model is a challenge. This paper discusses the usage of symbolic regression to learn hybrid systems from data and specifically analyses learning parameters for a recent algorithm. Symbolic regression is a powerful tool that can automatically discover accurate and interpretable mathematical models in the form of symbolic expressions. Models generated by symbolic regression are a valuable tool for system identification and diagnosis, e.g., to predict future system behavior or detect anomalies. A major opportunity of our approach is the ability to detect transitions between different continuous behaviors of a system directly based on the dynamics. From a diagnosis perspective, this can advantageously be used to detect the system entering fault modes and identify their models. This paper presents a parameter study for a symbolic regression based identification algorithm.

The early and automatic detection of faulty behavior is essential for maintaining the reliability of a cyber-physical system. In this paper we describe a fault localization approach for such a highly complex distributed system, the optical synchronization system of the European X-ray free-electron laser. Using a dependency graph, we model the relationships between the components and the influences of environmental effects. After we first resolve linear long-term dependencies between dependent components with a correlation analysis, we then use an unsupervised fault detection pipeline consisting of statistical feature extraction and unsupervised anomaly detection to accurately identify anomalies and localize their origins in the system.

Symbolic regression has shown potential in the identification of physical systems. Hybrid systems, which combine both continuous and discrete behavior, are a relevant extension of purely physical systems, used in many fields, including robotics, biological systems, and control systems. However, due to their complexity, finding an accurate model is a challenge. This paper presents a novel approach to learning models of hybrid systems using symbolic regression. Our method leverages the power of genetic programming to automatically discover accurate and interpretable mathematical models in the form of hybrid systems from observed data. Symbolic regression detects transitions between different continuous behavior of a system directly based on the dynamics, instead of pure distances of observed trajectories. Furthermore, models generated by symbolic regression can be used to predict future system behavior, detect anomalies, and identify the underlying dynamics of the system while providing a human-readable representation. Our results demonstrate that symbolic regression can effectively identify the underlying dynamics of a real system represented in a hybrid model, providing a valuable tool for system identification and diagnosis.

In the domain of cyber-physical systems, there is an increasing relevance of data-driven approaches for the learning of hybrid system dynamics. In particular, accurate models have been successfully abstracted from continuous (real-valued) traces and applied for various goals. However, industrial applications involving online modeling or rapid prototyping have two additional requirements: 1) runtime efficiency and 2) the interpretability of the approach and results.

This work develops an approach that lifts binaries into an enhanced LLVM Intermediate Representation (IR) including indirect jumps. The proposed lifter combines both static and dynamic methods and strives to fully recover the Control-Flow Graph (CFG) of a program. Using Satisfiability Modulo Theories (SMT) supported by memory and register models, our lifter dynamically symbolically executes IR instructions after translating them into SMT expressions.

Testing of black-box systems is a difficult task, because no prior knowledge on the system is given that can be used for design and evaluation of tests. Learning a model of a black-box system from observations enables model-based testing (MBT). We take a recent approach using decision tree learning to create a model of a black-box system and discuss the usage of such a decision tree model for test generation. In this scope, we define a test coverage metric for decision tree models. Furthermore, we identify different modes of testing and explain that a decision tree model especially facilitates model-based testing for black-box systems with limited controllability of inputs and the inability to reset the system to a specific state. A case study on a discrete system illustrates our MBT approach.

Decreasing the inference latency of neural networks is crucial in situations where real-time responses are necessary. We propose a new neuron architecture for parallel computations, targeting the MLP implementation on an FPGA. The parallelism in the proposed architecture is exposed through the segmentation of non-linear activation functions into a set of linear segments, delivering highly accurate estimations of the original function. The implementation combines various other optimization techniques, such as fixed-point arithmetics, pipelining, array partitioning, and loop unrolling. For the validation of the proposed architecture using the Xilinx Vitis HLS toolchain, four MLPs with a mix of non-linear activation functions have been implemented and evaluated in comparison to accelerated models produced by the open-source tool hls4ml, a Python package for latency-optimized machine learning inference in FPGAs. Experimental results clearly show that our proposed architecture outperformed the corresponding hls4ml model with up to three times speedups.

Ageing detection and failure prediction are essential in many Internet of Things (IoT) deployments, which operate huge quantities of embedded devices unattended in the field for years. In this paper, we present a large-scale empirical analysis of natural SRAM wear-out using 154 boards from a generalpurpose testbed. Starting from SRAM initialization bias, which each node can easily collect at startup, we apply various metrics for feature extraction and experiment with common machine learning methods to predict the age of operation for this node. Our findings indicate that even though ageing impacts are subtle, our indicators can well estimate usage times with an R2score of 0.77 and a mean error of 24% using regressors, and with an Fl score above 0.6 for classifiers applying a six-months resolution.

The successful operation of the laser-based synchronization system of the European X-Ray Free Electron Laser relies on the precise functionality of numerous dynamic systems operating within closed loops with controllers. In this paper, we present how data-based machine learning methods can detect and classify disturbances to such dynamic systems based on the controller output signal. We present 4 feature extraction methods based on statistics in the time domain, statistics in the frequency domain, characteristics of spectral peaks, and the autoencoder latent space representation of the frequency domain. These feature extraction methods require no system knowledge and can easily be transferred to other dynamic systems. We combine feature extraction, fault detection, and fault classification into a comprehensive and fully automated condition monitoring pipeline. For that, we systematically compare the performance of 19 state-of-the-art fault detection and 4 classification algorithms to decide which combination of feature extraction and fault detection or classification algorithm is most appropriate to model the condition of an actively controlled phase-locked laser oscillator. Our experimental evaluation shows the effectiveness of clustering algorithms, showcasing their strong suitability in detecting perturbed system conditions. Furthermore, in our evaluation, the support vector machine proves to be the most suitable for classifying the various disturbances.

Modeling Cyber-Physical Systems (CPS) requires knowledge from various domains, including computer science, electrical and mechanical engineering, and control theory. In addition, a solid understanding of the application domain, e.g., intralogistics, maritime technology, or grid control technology is required to ensure relevant and accurate models. In order to reduce the knowledge required for modeling CPS, we envision a framework for Automatic Generation of models for CPS (AGenC) supporting design and operation. Typical tasks in design and operation are summarized by the terms prediction, monitoring, and testing. Thus, the proposed framework employs learning techniques to generate models of CPS that predict the system’s performance in various scenarios, monitor the system in real-time to detect anomalies or failures, and automatically generate test cases. This research has the potential to significantly reduce the time and effort required for designing, testing, and maintaining CPS, making them more reliable and efficient.

For integrated circuits in vehicular systems, ISO 26262 requires fault injection. Failure modes in natural language specify potential malfunctions of components in an abstract system model. Fault injection in system models ensures that safety mechanisms are effective. This causes a gap in the design process as fault injection campaigns must be derived manually.We introduce the framework FINaL that drives high-level Fault Injection campaigns with Natural Language. FINaL starts from an abstract system model in SysML, requirements, and failure modes described in natural language. We explain how FINaL automatically derives the parameters required for fault injection campaigns on virtual prototypes in SystemC. After training on a simple reference design, experimental results demonstrate that 20% up to 67% of the failure modes for a productive design can automatically be handled.

Abstract models of embedded systems are useful for various tasks, ranging from diagnosis, through testing to monitoring at run-time. However, deriving a model for an unknown system is difficult. Generic learners like decision trees can identify specific properties of systems and have been applied successfully, e.g., for anomaly detection and test case identification. We consider Decision Tree Learning (DTL) to derive a new type of model from given observations with bounded history for systems that have a Mealy machine representation. We prove theoretical limitations and evaluate the practical characteristics in an experimental validation.

Cyber-Physical Systems (CPS) are often black-box systems, i.e., knowledge of the inner workings or a system model is not available. Nevertheless, models of CPS are needed for various tasks, ranging from verification, over testing to monitoring at runtime. For these tasks, finite and discrete models facilitating understandability, compactness, and efficiency are often desirable. Deriving a discrete model of a continuous-valued CPS is difficult. A simple abstraction is achieved with a time and value discretization through sampling and discretization intervals. We consider observing the system with bounded history and apply decision tree learning on discretized observations to generate a model of the system. The model supports the identification of system characteristics and predicts a valid next output based on the bounded history. We prove an upper bound on the error size for the prediction of an output. Experimental results give practical insight and present a comparison to automata learning.

Absolute position accuracy is the key performance criterion of an Indoor Localization System (ILS). Since ILS are heterogeneous and complex cyber-physical systems, the localization accuracy depends on various influences from the environment, system configuration, and the application processes. To determine the position accuracy of a system in a reproducible, comparable, and realistic manner, these factors must be taken into account. We propose a strategy for analyzing the influences on the position accuracy of ILS using decision trees in combination with application-related or technology-related categorization. The proposed strategy is validated using empirical data from 120 experiments. The accuracy of an Ultra-Wideband and a LiDAR-based ILS was determined under different application-driven influencing factors, considering the application of autonomous mobile robots in warehouses. Finally, the opportunities and limitations of analyzing decision trees to compare system performance, find a suitable system, optimize the environment or system configuration, and understand the relevance of different influencing factors are presented.

The European X-Ray Free-Electron Laser (EuXFEL) relies like other high integrity systems on several sub systems. The Low Level Radio Frequency (LLRF) sub system of the EuXFEL is responsible for the correct acceleration of electron bunches. The LLRF system comprises several embedded components that are directly connected to the accelerator hardware. Due to the high complexity of the LLRF system, unforeseen machine trips occur regularly.In this work we built the basis for a mechanism that automatically identifies faulty behavior of the embedded components. To achieve that, we performed two different experiments, where a faulty behavior was artificially injected to the system. We analyzed the experiment data, performed a feature extraction and applied different machine learning methods. We used basic anomaly detection and basic clustering methods for identifying the faulty data elements. Additionally, we used a support vector machine for modelling the systems behavior. The selected algorithms are compared with respect to their ability to classify LLRF data correctly.

In this paper we examine two case studies in which we learn finite state machines from models of CPS using automata learning. We explore how well automata learning is suited as an approach for learning CPS. What challenges and problems exist when trying to learn a model of a CPS using automata learning. Automata learning can reliably learn finite state machines of systems like embedded systems or software systems. CPS pose different challenges, like continuous components, for which different levels of abstractions and considerations have to be used, so the resulting finite state machines are useful representations of the systems. Through the small, yet insightful case studies we show examples of how automata learning can be applied to CPS and what information the resulting automata can represent.

Anomaly detection algorithms solve the problem of identifying unexpected values in data sets. Such algorithms have been classically used for cleaning unlabelled data sets from potentially unwanted values. However, the ability to detect outlying values in data sets can also be used to detect anomalies in systems. Semi-supervised anomaly detection algorithms learn from data for known correct behavior. Such algorithms have been used in various fields, e.g., system security, fault detection, medical applications.In this paper, we use the Area Under the Receiver Operating Characteristic (AUROC) score to evaluate algorithms for semi-supervised anomaly detection when applied to high-integrity distributed digital systems. We identify the relevant parameter for each algorithm and observe how the parameter influences the score and the runtime.

The design of energy- and area-efficient systems is important for modern technology. One approach to increase these efficiencies is approximate computing. During the last years, efficient approximations for combinational hardware components, e.g., adders or multipliers, have been proposed.We focus on quality metrics for the evaluation of approximations in sequential circuits with streaming in- and outputs. We propose the usage of sequence distance metrics for analysis of the sequential behavior after approximation and compare their performance to other metrics like mean errors and accumulated errors. We present case studies on some exemplary circuits. The experimental results show that our sequential metrics provide additional information to common mean errors and for stochastic applications yield the best guidance in selecting approximate sequential circuits.

Embedded systems play an important role in various tasks in many areas of our lives. In the case of safety-critical applications, e.g., in the fields of autonomous driving, medical devices or control of unmanned aerial vehicles (UAV), the correct system operation must always be guaranteed. Standard methods for monitoring an embedded application, i.e., detecting erroneous behavior at run-time, require a detailed system understanding during development which increases the design effort significantly.Our approach uses Artificial Neural Networks (ANN), specifically recurrent Long Short-Term Memory (LSTM) architectures, to realize cost efficient monitoring for embedded systems. We propose extensions to existing ANN-based monitoring approaches and investigate suitable ANN architectures, which facilitate fault detection on the open-source UAV flight stack PX4. We demonstrate that our ANN-based approach can detect faults on a raw data stream coming from the monitored system, thus minimizing the need to engineer curated data streams in order to adapt the approach to a different device.

The problem of generating a minimal implementation of a given Boolean function is called exact synthesis. The parameter to be minimized is often the total number of gates used for the implementation. The exact synthesis engine is considered an essential tool for most state-of-the-art logic optimization flows. In this paper, we present an algorithm that, using enumeration over non-isomorphic graph structures, generates minimal circuits implementing specified Boolean functions using a set of predefined gate types. In our experiments, we show that our prototype implementation of this technique can be compared to state-of-the-art tools for small functions. Moreover, we show that this technique can be parallelized effectively.

Reliability, security, and safety become even more challenging in times of the Internet of Things (IoT). Devices operate jointly in large distributed networks and may affect each other's functionality due to failures or attacks. Identifying abnormal system behavior is therefore the solution to protect the device itself and other network participants to ensure service availability and system integrity. We propose a monitor concept based on long short-term memory recurrent neural networks which adapts to new devices by learning the nominal behavior automatically. No fault model is needed to identify erroneous behavior. The monitor can operate locally on the device, so our approach addresses the limited bandwidth and connectivity of IoT devices. Experiments evaluate our approach for a simulated controller under varying runtime conditions.

Tools for Automatic Test Pattern Generation (ATPG) typically abstract timing. When a more detailed timing model is needed, either simulation or statistic timing analysis is usually applied. Our symbolic engine based on Satisfiability Modulo Theories can reason over a model using pin-to-pin timing arcs as available after synthesis or after place and route. We study the differences of a simple fixed gate delay versus the arc-based timing model.

We propose Syntax-Guided Property Enumeration, a method for automatically obtaining a set of short and readable temporal logic properties from sequential logic networks. Each property is a temporal logic formula which describes a relation between the primary inputs, the primary outputs, and the latches of the network over time. The approach is applicable to any temporal logic for which decision procedures for model-checking and satisfiability are available. In a case study, we analyze a generic USB controller and compare the results to the well-known previous approach GoldMine. We demonstrate how the flexibility of this approach helps the designer obtain different perspectives of the design under analysis. Useful applications are debugging, reverse engineering, security analysis, or specification mining.

Several approaches exist for specification mining of hardware designs, both at the RTL and system levels (e.g, TLM). These approaches mine assertions that specify the behavior of the design. Some of the techniques require the source code itself while others can extract assertions directly from simulation traces. The performance of some approaches is highly dependent on the number of simulation traces/use cases while there exist approaches which can extract assertions from a limited number of simulation traces. Apart from this aspect, the core of each assertion miner is different from the other ones. Some use expression templates to define assertions while some are based on the static analysis or information flow analysis. Unfortunately, it has been rarely considered which of the current approaches are more effective in describing functionality of particular types of designs. Thus, in this work, we analyze assertion miners which are template based and dynamic dependency graph based, respectively. We generate assertions from both approaches. The evaluation considers fault analysis on both assertion sets of extracted assertions. Moreover, both sets are combined and fault analysis has been applied on them. Experimental results show that each set approximately detects the same number of faults while when the two sets are combined the number of detected faults increases. Finally, a new, more efficient architecture for an effective assertion miner has been developed based on the study in this work.

Abstract Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults ineveryrealization of the specification and foreverybehavior of the uncontrollable part of the system’s environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. We argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies areadaptive test strategiesthat react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.

Handling faults in computing systems is often expensive in terms of power, area and financial costs. In domains requiring high reliability in harsh environments, like the space domain, special highly reliable components are used, which may adversely impact the processing performance. In this paper, we propose the STROBES algorithm for fault handling in a multi-node embedded system which can be composed of standard commercial off-the-shelf components. In particular, it does not require underlying synchronization, but relies on embedded system's properties to derive bounds for communication and processing times. The algorithm can handle asynchronous behavior between the nodes up to user-defined bounds, in addition to a fault in the state or fail-stop failure of a single node. Theoretical analysis shows that this is sufficient for extended operating times. Experimental data show the efficient behavior of the STROBES algorithm for practical application with different state and time bounds.

All solutions SAT (All-SAT) is important in applications where we require enumerating all satisfying assignments of a propositional formula, e.g., when reasoning over many or all possible test patterns in Automatic Test Pattern Generation (ATPG). We applied structural analysis starting from primary inputs or primary outputs to generalize a current total assignment to a partial assignment. This speeds up the determination of all satisfying assignments. The experiments were conducted using a large number of random instances and different available All-SAT solvers. We show that structural analysis techniques can significantly speed up enumeration of all satisfying assignments of combinational circuits and yield the the second largest number of total satisfying assignments from all compared All-SAT solvers.

We present an outline of the field of Design Understanding and summarize state-of-the-art research in deriving human-understandable knowledge in form of logic properties from an unknown design.

We present a technique to automatically generate System Verilog-Assertions from designs using dynamic dependency graphs. We extract relations between signals of the design using only a few simulation runs, which drastically reduces the required number of use cases compared to other approaches. Additionally, unlike previous approaches, we do not use expression templates to establish those relations. We abstract from the concrete use cases by inserting symbolic values and by merging similar conditions in time. A model-checker verifies the correctness of the generated properties. The evaluation shows that our approach is able to create more expressive properties than state of the art techniques, while requiring less simulation data.

The Exists-Forall (EF) synthesis problem deals with finding parameters such that for all input assignments a correctness specification is met. Many standard problems from computer-aided design and verification can be formulated as an instance of EF synthesis when a function template with holes - parameters to be synthesized - is provided. In this paper, we generalize the idea of EF synthesis in the context of Boolean logic by allowing existential quantification over the domain of Boolean functions (rather than Boolean variables) and present a bounded synthesis approach guided by counterexamples to generate them using techniques from Boolean learning. As an application, we present circuit rectification as an EF synthesis problem and apply the presented approach to incrementally synthesize patches for digital circuits with multiple seeded faults.

Before a microchip's concrete implementation is available a very abstract model is created, e.g., on Electronic System Level (ESL) or even more abstract. To ensure a better design understanding, we propose an automated mapping from a given abstract model to an unfamiliar concrete implementation at Register Transfer Level (RTL). But how to map a variable from the abstract model to a variable from the concrete model? We address this problem by a simulation based approach. We instrument the abstract model to get traces for each variable in both models and propose four heuristics to evaluate which variable maps to a corresponding variable of the other model. Experiments on an Instruction Set Simulator (ISS) versus RTL processor show mappings which offer an insight into the RTL implementation.

Current transients caused by energetic particle strikes are a serious threat for digital circuits in aerospace applications. Such single-event transients (SETs) can corrupt the circuit state, with possibly devastating consequences. Although it is possible to protect circuits with spatial redundancy techniques, the area and power overhead is high. Therefore aerospace circuits would benefit from adopting temporal redundancy instead, but existing solutions prioritize performance over reliability. Our proposed temporal redundancy latch-based architecture (TRLA) is a standard cell, static CMOS temporal redundancy technique, with area savings of 26%, power savings of 46%, and 14% faster circuit operation compared to triple modular redundancy (TMR).

Local triple modular redundancy (LTMR) is often the first choice to harden a flash-based FPGA application against soft errors in space. Unfortunately, LTMR leads to at least 300% area overhead. We propose a parity-based error detection approach, to use the limited resources of space-proven flash-based FPGAs more area-efficiently; this method can be the key for fitting the application onto the FPGA. A drawback of parity-based hardening is the significant impact on the critical path. To alleviate this error detection latency, pipeline structures in the design can be utilized. According to our results, this eliminates from 22% to 65% of the critical path overhead of the unpipelined error detection. Compared with LTMR, the new approach increases the critical path overhead of LTMR by a factor varying from 2 to 7.

As systems become more complex, the size of transistors decreases. This effect leads to an increased probability of transient faults as well as higher variability of the transistors. Verifying that circuits are robust against transient faults and variability is mandatory. While formal verification may be used to prove robustness, a model that includes extracted electrical parameters and the corresponding timing information is usually too complex in practice. The contribution of this paper consists in a hybrid algorithm that can decide robustness. The algorithm uses Boolean reasoning as well as simulation to decompose the problem into feasible SAT formulas and still achieves completeness. In our experiments, we compare the algorithm against our previous implementation and achieve an average speed up of 1500 on the ISCAS-85 benchmarks and fault tolerant modifications.

CPS, that consist of a cyber part – a computing system – and a physical part – the system in the physical environment – as well as the respective interfaces between those parts, are omnipresent in our daily lives. The application in the physical environment drives the overall requirements that must be respected when designing the computing system. Here, reliability is a core aspect where some of the most pressing design challenges are: monitoring failures throughout the computing system, determining the impact of failures on the application constraints, and ensuring correctness of the computing system with respect to application-driven requirements rooted in the physical environment. This paper provides an overview of techniques discussed in the special session to tackle these challenges throughout the stack of layers of the computing system while tightly coupling the design methodology to the physical requirements.

We propose EASY, an algorithm for functional equivalence checking of ESL descriptions written in a high-level programming language like C++. Given two ESL descriptions, in a PDR-like fashion EASY systematically refines a candidate invariant to characterize the reachable states of a miter of the descriptions until either the invariant becomes inductive or a counterexample has been found. The algorithm is flexible and allows to incorporate a priori knowledge about the design to speed up the verification process. We provide an implementation of EASY on top of a standard model checker and show in two case studies that EASY outperforms other state-of-the-art equivalence checking tools.

We present an outline of the field of Multilevel Design Understanding by first defining and motivating the related problems, and then describing the key issues which must be addressed in future research.

We propose an exact algorithm to model-free diagnosis with an application to fault localization in digital circuits. We assume that a faulty circuit and a correctness specification, e.g., in terms of an un-optimized reference circuit, are available. Our algorithm computes the exact set of all minimal diagnoses up to cardinality k considering all possible assignments to the primary inputs of the circuit. This exact diagnosis problem can be naturally formulated and solved using an oracle for Quantified Boolean Satisfiability (QSAT). Our algorithm uses Boolean Satisfiability (SAT) instead to compute the exact result more efficiently. We implemented the approach and present experimental results for determining fault candidates of digital circuits with seeded faults on the gate level. The experiments show that the presented SAT-based approach outperforms state-of-the-art techniques from solving instances of the QSAT problem by several orders of magnitude while having the same accuracy. Moreover, in contrast to QSAT, the SAT-based algorithm has any-time behavior, i.e., at any-time of the computation, an approximation of the exact result is available that can be used as a starting point for debugging. The result improves while time progresses until eventually the exact result is obtained.

High compression ratio is crucial to cope with the large amounts of data produced by telemetry sensors and the limited transmission bandwidth typical of space applications. A new generation of telemetry units is under development, based on Commercial Off-The-Shelf (COTS) components that may be subject to misbehaviors due to radiation-induced soft errors. The purpose of this paper is to study the impact of soft errors on different configurations of a discrete cosine transform (DCT)-based compression algorithm. This work's main contribution lies in providing some design guidelines.

We propose an approach for overapproximating the Worst-Case Execution Time (WCET) of embedded control software using formal methods. Model checking is iteratively applied to compute the WCET from the machine code of the software considering a platform and an environment model. We implemented the approach and present first experiments for a thermal controller application executed on a LEON3 processor under different environment constraints.

Diagnosis of integrated circuits is an arduous process. Tools are needed which aid developers locating circuit's faulty parts faster. In this work path delay faults are considered. A simulation based diagnosis algorithm using diagnostic test patterns is introduced for locating the cause of the delay fault. Initial paths are segmented to improve the diagnosis accuracy. For each segment, additional diagnostic test patterns are generated using a solver for Boolean Satisfiability. The experimental results show that a significant improvement of the diagnostic accuracy is achievable with our approach.

Equivalence checking is applied when a system description is refined iteratively to reduce the manual effort required to check the consistency before and after modifications. We present a novel functional equivalence checking algorithm which is especially designed to verify equivalence of two hardware descriptions on the system level. Our algorithm uses a stepwise induction proof guided by counterexamples and incorporates a priori knowledge provided by a designer to speed up reasoning. The a priori knowledge is given symbolically in form of a hypothesis, i.e., A logical formula, which approximates the set of all possible equivalence states of the two designs. The algorithm step wisely refines the hypothesis until either a counterexample has been found disproving equivalence or the hypothesis over approximating all equivalence states. Preliminary experiments for two case studies, a scalable parallel counter and a processor model, show the applicability of our approach in practice.

In modern chip design, many different blocks are assembled in a single chip. Normally, these blocks have been written by different developers or even licensed from other companies. Correctly connecting all blocks is a tedious task. State of the art tools for automatically generating the connections either require identical port-names or additional user input describing the intended connections.

A major concern in the design of high performance VLSI circuits is speedpath debugging. This is due to the fact that timing variations induced by process variations and environmental effects are increasing as the size of VLSI circuits is shrinking. In this paper, a speedpath debugging approach based on Boolean Satisfiability (SAT) is proposed. The approach takes waveforms of the signals of a circuit into account. Waveforms and their propagation are encoded using SAT. Also, timing variation models for slowdown and speedup of each gate are incorporated into the model. The whole timing variation is controlled by a unit called variation control. Having an Erroneous Trace (ET) due to timing variation, our debug engine automatically finds potential failing speedpaths. The experimental results on ISCAS benchmarks show efficiency and diagnosis accuracy of our approach. The approach can also localize potential failing speedpaths for the multiplier circuit c6288 that has a large number of paths.

Various problems from artificial intelligence and formal methods are solved utilizing Satisfiability Modulo Theories (SMT) solvers. Selecting the best SMT solver for a specific application, however, is a daunting task. In this paper, we present the novel metaSMT TCP server and client architecture which can be used to solve SMT instances expressed in SMT-LIB2 by multiple solver processes in parallel. The metaSMT TCP server provides a unified interface for SMT-LIB2 instances with the capability to either use the API or the file interface of a solver process and thus serves as a highly customizable portfolio solver. We show that the run-time overhead required by the metaSMT TCP server and client architecture is marginal using selected benchmarks from SMT-LIB.

As complexity and size of Systems-on-Chip (SoC) grow, debugging becomes a bottleneck for designing IC products. In this paper, we present an approach for online debug of NoC- based multiprocessor SoCs. Our approach utilizes monitors and filters implemented in hardware. Monitors and filters observe and filter transactions at run-time. They are connected to a Debug Unit (DU). Transaction-based programmable Finite State Machines (FSMs) in the DU check assertions online to validate the correct relation of transactions at run-time. The experimental results show efficiency and performance of our approach.

Verifying correctness is a major bottleneck in today's circuit and system design. Verification includes the tasks of error detection, error localization, and error correction in an implemented design, as well as the analysis and avoidance of transient faults. For all those tasks, knowing when an assignment to signals becomes observable at the outputs and for how long it influences the system is important. In this letter, we propose a minimal and maximal latency measure for sequential circuits. This measure explains how long a circuit's state and outputs depend on input stimuli. Exact and heuristic algorithms are discussed to determine the measure. We evaluate the algorithms on state-of-the-art designs. Experimental results show how the measure provides insight into the behavior of circuit designs.

The complexity of modern chips is rapidly increasing. To fulfill tight time-to-market constraints, more and more blocks from previous designs are reused or third party IP blocks are licensed. However, such blocks are often only poorly documented making adjustments to the blocks a difficult task. This paper presents a technique for automatic feature localization for hardware designs. Our approach helps a developer in understanding a design by localizing parts of the code which implement a certain feature of interest. We evaluate the approach on three open source designs. For those designs, our approach yields a more precise localization of the code implementing the different features than the documentation of the design.

In safety related applications and in products with long lifetimes reliability is a must. Moreover, facing future technology nodes of integrated circuit device level reliability may decrease, i.e., counter-measures have to be taken to ensure product level reliability. But assessing the reliability of a large system is not a trivial task. This paper revisits the state-of-the-art in reliability evaluation starting from the physical device level, to the software system level, all the way up to the product level. Relevant standards and future trends are discussed.

Modern chip designs are getting more and more complex. To fulfill tight time-to-market constraints, third-party blocks and parts from previous designs are reused. However, these are often poorly documented, making it hard for a designer to understand the code. Therefore, automatic approaches are required which extract information about the design and support developers in understanding the design. In this paper we introduce a new dynamic data flow analysis tuned to automate design understanding. We present the use of the approach for feature localization and for understanding the design's data flow. In the evaluation, our analysis improves feature localization by reducing the uncertainty by 41% to 98% compared to a previous approach using coverage metrics.

Embedded systems consist of hardware and software and are ubiquitous in safety-critical and mission-critical fields. The increasing integration density of modern, digital circuits causes an increasing vulnerability of embedded systems to transient faults. Techniques to improve the fault tolerance are often either implemented in hardware or in software. In this paper, we focus on synthesis techniques to improve the fault tolerance of embedded systems considering hardware and software. A greedy algorithm is presented which iteratively assesses the fault tolerance of a processor-based system and decides which components of the system have to be hardened choosing from a set of existing techniques. We evaluate the algorithm in a simple case study using a Traffic Collision Avoidance System (TCAS).

Speedpath diagnosis is one of the major challenges in designing high-performance Very-Large-Scale Integrated (VLSI) circuits due to timing variations caused by process variations and environmental effects. In this paper, an efficient approach to automate speedpath debugging is presented. The approach relies on converting the timing behavior of a circuit and its corresponding timing variations into functional domain. Afterwards, a SAT-based debug engine is utilized to extract potential failing speedpaths. The experimental results on ISCAS'85 and ISCAS'89 benchmark suites show that our approach achieves a 63% decrease in the size of model resulting in 54% decrease in the debugging time compared to previous work while having a high diagnosis accuracy.

The increasing complexity of circuits and systems is forcing design specifications to software-like programming languages like C. Since the conversion from software to hardware is a difficult task solved manually, bugs are frequently introduced in the HDL design. Sophisticated automated error localization and correction techniques, i.e. debugging, are a challenge. In this paper a new automated method is presented for debugging hardware implementations when a software-like specification in C is given. Based on functional equivalences between software and hardware, error localization and correction are automated. We present experimental results for different types of designs and different types of faults.

Debugging of speed-limiting paths (speed paths) is a key challenge in development of Very-Large-Scale Integrated(VLSI) circuits as timing variations induced by process and environmental effects are increasing. This paper presents an approach to diagnose speed paths under timing variations. First timing behavior of a circuit and corresponding variation models are converted into a functional domain. Then, our automated debugging based on Boolean Satisfiability (SAT) diagnoses speed paths. The experimental results show the effectiveness of our approach on ISCAS'85 and ISCAS'89 benchmarks suites. In average, the diagnosis accuracy of 98:51% is achieved by our approach.

Due to the increasing complexity modern System on Chip designs are developed by large design teams. In addition, existing design blocks are re-used such that the knowledge about these parts of the design entirely depends on the quality of the documentation. For a single designer it is almost impossible to have detailed knowledge about all blocks and their interaction.

Due to the increasing design size and complexity of modern Integrated Circuits (IC) and the decreasing time-to-market, debugging is one of the major bottlenecks in the IC development cycle. This paper presents a generalized approach to automate debugging which can be used in different scenarios from design debugging to post-silicon debugging. The approach is based on model-based diagnosis. Diagnostic traces are proposed as an enhancement reducing debugging time and increasing diagnosis accuracy. The experimental results show the effectiveness of the approach in post-silicon debugging.

This paper presents a methodology to model and analyze the functional behavior of logic circuits under timing variations. In the framework, first a Time Accurate Model (TAM) of the circuit is constructed. The TAM represents the behavior of the circuit in the functional domain under a discrete time model. Afterwards, Variation Logic is inserted to apply the timing variations. Moreover, the circuit TAM is enhanced by Time Control (TC) logic to model the circuit frequency. We apply the proposed methodology to analyze a circuit or an approximate circuit under timing variations as well as to analyze a circuit under timing-induced errors for approximate computing.

Summary form only given. This work proposes an approach to model and evaluate the functional behavior of logic circuits under timing variations. In the approach, first we construct a Time Accurate Model (TAM) of the circuit to represent its timing behavior in a functional domain under a discrete time model. Then, timing variations are applied by using Variation Logic (VL).

Debugging techniques assist a developer in localizing and correcting faults in a system's description when the behavior of the system does not conform to its specification. Two fault localization techniques are model-based diagnosis and error explanation. Model-based diagnosis computes a subset of the system's components which when replaced correct the system. Error explanation determines potential causes of the system's misbehavior by comparing faulty and correct execution traces. In this paper we focus on fault localization for imperative, non-concurrent programs. We compare the two fault localization techniques in a unified setting presenting SAT-based algorithms for both. The algorithms serve as a vantage point for a fair comparison and allow for efficient implementations leveraging state-of-the-art decision procedures. Firstly, in our comparison we use constructed programs to study strengths and weaknesses of the two fault localization techniques. We show that in general none of the fault localization techniques is superior but that the computed fault candidates depend on the program structure. Secondly, we implement the SAT-based algorithms in a prototype tool utilizing a Satisfiability Modulo Theories (SMT) solver and evaluate them on mutants of the ANSI-C program TCAS from the Software-Artifact Infrastructure Repository (SIR).

Complex Systems on Chip are developed by large design teams integrating various different blocks. Typically, no single person in the design team understands all details of such a design. Integrating new designers into the team as well as debugging failures or performance problems becomes a time-consuming cost-generating threat to the overall project.

The automatic verification of designs is a challenging task and of high interest due to increasing time-to-market constraints. In this paper, we focus on the verification of bus bridges which are used in many hardware systems to connect two buses running different protocols. We developed an approach to assist the automatic generation of properties from the protocol specification for the formal verification of bus bridges. The technical contribution is that the final set of the verification suite is functionally complete in respect to the underlying verification tool which shows the absence of any verification holes. The approach uses an abstract model of bus bridges in terms of state machines which enables a generic work flow. In experimental evaluations we applied the approach to bus bridges based on the OCP/IP protocol family.

Debugging is one of the major bottlenecks in the current VLSI design process as design size and complexity increase. Efficient automation of debugging procedures helps to reduce debugging time and to increase diagnosis accuracy. This work proposes an approach for automating the design debugging procedures by integrating SAT-based debugging with test bench based verification. The diagnosis accuracy increases by iterating debugging and counterexample generation, i.e., the total number of fault candidates decreases. The experimental results show that our approach is as accurate as exact formal debugging in 71% of the experiments.

Verification is a major bottleneck in today's circuit and system design. This includes the tasks of error detection, error localization, and error correction in an implemented design as well as the analysis and avoidance of transient faults. For all those tasks, knowing for how long values of signals influence the system is important. In this paper, we propose a minimal and maximal latency measure for sequential circuits. This measure explains how long a circuit's state and outputs depend on input stimuli. Exact and heuristic algorithms are proposed to determine the measure. Experiments show that the measure provides insight into the behavior of circuit designs.

Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults, e.g., due to environmental radiation. Approaches to implement fault tolerance are known. But assessing the fault tolerance of a given implementation is a hard verification problem. Here, we propose the use of formal methods to assess the robustness of a digital circuit with respect to transient faults. Our formal model uses a fixed bound in time and exploits fault detection circuitry to cope with the complexity of the underlying sequential equivalence check. As a result, a lower and an upper bound on the robustness are returned together with vulnerable components. The underlying algorithm and techniques to improve the efficiency are presented. In experiments, we evaluate the method on circuits with different fault detection mechanisms.

Summary form only given. Modern circuits contain up to several hundred million transistors and this number grows exponentially over time. Thus, the state-of-the-art design flows have to be improved continuously. In the meantime ensuring correctness becomes a major bottleneck. Up to 80% of the overall design costs are due to verification and even more problems are foreseeable - shrinking feature sizes lead to large process variations, increased susceptibility to radiation, etc. As a result even a correct design may contain faulty components. Thus, robustness is required, i.e. correct operation in presence of faults. Formal verification techniques have gained large attention, since they allow proving the correctness of a circuit and thereby ensure 100% functional correctness. Moreover, the underlying techniques can also be used to prove robustness of a design. Besides being more reliable, formal verification approaches have also shown to be more cost effective in many cases, since test bench creation - usually a very time consuming and error prone task - becomes superfluous. Therefore these techniques allow unveiling faulty behaviour automatically. Proving robustness in the sense of fault tolerance is important. As in any implementation step, faults may tamper the behaviour. In particular, fault tolerance may hide flaws during the standard verification step. Therefore instead of relying on the design's architectural precautions against faults, the implementation has to be proven to be fault tolerant. In this tutorial, after a brief motivation of the overall topic and definition of the problem domain, the alternative verification approaches are explained. Next, the application of the underlying formal techniques for robustness checking is considered. The standard approaches for verification are simulation, emulation and formal methods. Details are discussed related to formal verification, symbolic simulation and assertion based verification. The verification scenarios for equivalence checking (EC) and property checking (PC) are presented and the underlying proof techniques are explained. Robustness checking then also builds on the underlying formal methods. This allows analyzing the robustness of a design fully automatically. Practical scenarios covered by this model for robustness of a circuit are discussed. The model not only yields a measure for the robustness of a circuit but also shows critical parts of the implementation that should be reengineered. In comparison alternative approaches, e.g. using statistical measures, are outlined. Further references are given for all topics are given (see below). Directions for future work and research challenges are discussed.

In presence of increasing soft error rates due to shrinking feature sizes, design tools are required to analyze fault tolerance and robustness of circuits. Here, we propose a new measure that identifies hot-spots in the design. On the one hand the measure is more accurate than a "worst-case analysis" that ignores excitation probabilities. On the other hand the computation of the new measure is more efficient than a "probabilistic analysis" that considers excitation probabilities at the cost of a higher computational complexity. Both of these extremes can be embedded in the new measure. Experimental results on circuits with protection against soft errors show that the new measure can be calculated effectively.

Continuously shrinking feature sizes cause an increasing vulnerability of digital circuits. Manufacturing failures and transient faults may tamper the functionality. Automated support is required to analyze the fault tolerance of circuits. In this paper, Robu Check is presented - a design tool to analyze the fault tolerance of digital circuits. Engines based on simulation and formal methods are integrated to identify components that require additional fault protection. Consequently, an overall estimation of fault tolerance of the circuit is determined.

For a variety of signal processing applications polynomials are implemented in circuits. Recent work on polynomial datapath optimization achieved significant reductions of hardware cost as well as delay compared to previous approaches like Horner form or Common Sub-expression Elimination (CSE). This work 1) proposes a formal model for single- and multi-polynomial factorization and 2) handles optimization as a constraint solving problem using an explicit cost function. By this, optimal datapath implementations with respect to the cost function are determined. Compared to recent state-of-the-art heuristics an average reduction of area and critical path delay is achieved.

Debugging significantly slows down the design process of complex systems. Only limited tool support is available and often fixing one problem leads to finding the next one. Here, we propose an approach that integrates formal verification with diagnosis. The approach is based on Quantified Boolean Formulas (QBF) and ensures, that counterexamples of high quality are returned. Moreover, the diagnosis algorithm only returns fault candidates that can fix all counterexamples. By this, the total number of fault candidates decreases and less iterations between verification and debugging are required.

Measuring the steady state leakage current (IDDQ) is very successful in detecting faults not discovered by standard fault models. But vector dependencies of IDDQ decrease the resolution. We propose deterministic ATPG algorithms to create test vectors within predefined leakage ranges. Even when random pattern generation does not find test vectors, the proposed algorithms identify vectors within the desired range. Experimental results confirm that leakage constraints are effectively handled during test pattern generation without decreasing fault coverage.

Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults, e.g. due to environmental radiation. Approaches to implement fault tolerance are known. But assessing the fault tolerance of a given circuit is a tough problem.

Equivalence checking and property checking are powerful techniques to detect error traces. Debugging these traces is a time consuming design task where automation provides help. In particular, debugging based on Boolean satisfiability (SAT) has been shown to be quite efficient. Given some error traces, the algorithm returns fault candidates. But using random error traces cannot ensure that a fault candidate is sufficient to explain all erroneous behaviors. Our approach provides a more accurate diagnosis by iterating the generation of counterexamples and debugging. This increases the accuracy of the debugging result and yields more valuable counterexamples. As a consequence less time consuming manual iterations between verification and debugging are required - thus the debugging productivity increases.

Feature sizes in VLSI circuits are steadily shrinking. This results in increasing susceptibility to soft errors, e.g. due to environmental radiation. Precautions against soft errors can be taken on all design stages, e.g. the architectural level, algorithmic level, or on the layout level. Whether the final implementation contains flaws or really provides robustness to soft errors remains to be checked. Here, we propose an approach to formally verify the robustness of a circuit with respect to multiple soft errors. We propose a fault model that prunes the exponentially sized space of multiple soft errors and an algorithm that automatically analyzes a given circuit.

In previous technology generations IDDQ testing used to be a powerful technique to detect physical faults that are not covered by standard fault models or functional tests. Due to shrinking feature sizes and consequently increasing leakage currents IDDQ testing becomes difficult in the deep-sub-micron area. One of the problems is the vector dependency of leakage current. Even in good devices the leakage current may vary significantly from one test vector to the next. In this work we present an ATPG framework that allows to generate test vectors within tight constraints on leakage currents. The target range for the leakage current is automatically determined. Experiments on the ITC99 benchmark suite yield test sets that achieve 100% fault coverage for the larger circuits, even when the range is narrowed down to 50% of the standard deviation of random vectors.

Property checking is a promising approach to prove the correctness of today's complex designs. However, in practice this requires the formulation of formal properties which is a time consuming and non-trivial task. Therefore the acceptance and efficiency of formal verification techniques can be raised by an automated support for formulating design properties. In this paper we propose a new methodology to automatically generate complex properties for a given design. The tool, Dianosis, implements this methodology by analyzing a simulation trace. The extracted properties describe the abstract design behavior and are presented in a format that is easy to read and can be added to the set of properties used for formal or assertion-based verification. We provide experimental results on industrial hardware designs that show the effectiveness of Dianosis and motivate the practical use.

Integrating design and verification becomes more and more important due to the increasing complexity of today's circuits and systems. SystemVerilog is a description language that embeds verification goals with the help of SystemVerilog assertions (SVAs). Often SVAs are used in simulation-based verification. But in the past first applications in formal verification have been considered, too. In this paper we present an approach to prove SVAs by induction based bounded model checking (BMC). Since checking SVAs is computationally very complex, we define a subset which is sufficient for many practical purposes. For each restriction a rationale is given.The creation of the BMC instance for this subset is explained in detail. Case studies show the application of our approach.

Due to the increasing complexity of today's circuits a high degree of automation in the design process is mandatory. The detection of faults and design errors is supported quite well using simulation or formal verification. But locating the fault site is typically a time consuming manual task. Techniques to automate debugging and diagnosis have been proposed. Approaches based on Boolean Satisfiability (SAT) have been demonstrated to be very effective. In this work debugging on the gate level is considered. Unsatisfiable cores contained in a SAT instance for debugging are used (1) to determine all suspects, and (2) to speed-up the debugging process. In comparison to standard SAT-based debugging, the experimental results show a significant speed-up for debugging multiple faults.

Due to the rapidly growing size of integrated circuits, there is a need for new algorithms for automatic test pattern generation (ATPG). While classical algorithms reach their limit, there have been recent advances in algorithms to solve Boolean Satisfiability (SAT). Because Boolean SAT solvers are working on conjunctive normal forms (CNFs), the problem has to be transformed. During transformation, relevant information about the problem might get lost and, therefore, is not available in the solving process. In this paper, we present a technique that applies structural knowledge about the circuit during the transformation. As a result, the size of the problem instances decreases, as well as the run time of the ATPG process. The technique was implemented, and experimental results are presented. The approach was combined with the ATPG framework of NXP Semiconductors. It is shown that the overall performance of an industrial framework can significantly be improved. Further experiments show the benefits with regard to the efficiency and robustness of the combined approach.

We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results.

During synthesis of circuits for Boolean functions area, delay and testability are optimization goals that often contradict each other. Multi-level circuits are often quite small while circuits with low depth are often larger regarding the area requirements. A different optimization goal is good testability which can usually only be achieved by additional hardware overhead. In this paper we propose a synthesis technique that allows to trade-off between area and delay. Moreover, the resulting circuits are 100% testable under the stuck-at fault model. The proposed approach relies on the combination of 100% testable circuits derived from binary decision diagrams and 2-SPP networks. Full testability under the stuck-at fault model is proven and experimental results show the trade-off between area and depth.

Due to the development of high speed circuits beyond the 2-GHz mark, the significance of automatic test pattern generation for path delay faults (PDFs) drastically increased in the last years. This paper describes an algorithm for generating robust and non-robust tests for PDFs based on Boolean satisfiability (SAT). A new formulation for the robust path delay fault model as a SAT instance is introduced. Unlike previous SAT-based approaches our approach can cope with latches and is therefore applicable for sequential circuits. The formulation provides the possibility to apply the SAT technique incremental SAT to accelerate the process. Experimental results show the efficiency of the approach.

Due to the rapidly growing speed and the decreasing size of gates in modern chips, the probability of faults caused by the production process grows. Already small variations lead to functional failures. Therefore, dynamic fault models like the path delay fault model (PDFM) have become more important in the last years. At the same time, classical algorithms for test pattern generation reach their limits due to the steadily increasing complexity of modern circuits. In this work, a SAT-based approach to calculate robust and non-robust test patterns for path delay faults (PDF) is presented. In contrast to previous approaches, the sequential behavior of a circuit is modeled adequately. Moreover, tri-state elements and environment constraints that occur in industrial practice can be handled. The encoding to apply a Boolean SAT solver for this problem is motivated and explained in detail. Experimental results for large industrial circuits show the efficiency of this approach.

Solvers for Boolean Satisfiabilily (SAT) are state-of-the-art to solve verification problems. But when arithmetic operations are considered, the verification performance degrades with increasing data-path width. Therefore, several approaches that handle a higher level of abstraction have been studied in the past. But the resulting solvers are still not robust enough to handle problems that mix word level structures with bit level descriptions. In this paper, we present the satisfiability solver SWORD — a SAT like solver that facilitates word level information. SWORD represents the problem in terms of modules that define operations over bit vectors. Thus, word level information and structural knowledge become available in the search process. The experimental results show that on our benchmarks SWORD is more robust than Boolean SAT, K⋆BMDs or SMT.

During bounded model checking (BMC) blocks of a design are often considered separately due to complexity issues. Because the environment of a block is not available for the proof invalid input sequences frequently lead to false negatives, i.e. counter-examples that can not occur in the complete design. Finding and understanding such false negatives is currently a time-consuming manual task. Here, we propose a method to automatically avoid false negatives which are caused by invalid input sequences for blocks connected by standard communication protocols

The problem of diagnosis - or locating the source of an error or fault $occurs in several areas of computer aided design, such as dynamic verification, property checking, equivalence checking and production test. Manually locating errors can be a time consuming and resource-intensive process. Several automated approaches for diagnosis have been presented, among them are simulation-based and SAT-based techniques. These two approaches are found to be robust even for large circuits as well as being applicable to a broad range of diagnosis problems. An in-depth comparison of both approaches necessary to augment our knowledge of diagnosis procedures has not been addressed by previous work. This paper provides a thorough analysis of the similarities and differences between simulation-based and SAT-based procedures for diagnosis. The relation between the basic approaches is theoretically analyzed. Issues regarding performance and diagnosis quality (resolution) are discussed. Experimental data strengthens the theoretical results. This detailed understanding of the relations between the techniques is necessary to provide further improvements to the field of diagnosis. The initial steps towards building a hybrid technique are also presented

The complexity of circuit and systems design increases rapidly. Therefore, a main focus of research in the area of electronic-design automation are efficient algorithms and data structures. Among these, binary decision diagrams (BDDs) have been used in a wide variety of applications and were intensively studied from a theoretical point of view. But mostly, when complexity issues were considered, only the number of nodes in a BDD has been analyzed. Here, we study minimizing the number of paths in BDDs from a theoretical and a practical point of view. Connections to different areas in computer-aided design are outlined, theoretical studies are carried out, and an algorithm to minimize the number of paths is presented. Experimental results show the efficiency of the algorithm.

In this paper we study the testability of circuits derived from Binary Decision Diagrams (BDDs) under the bridging fault model. It is shown that testability can be formulated in terms of symbolic BDD operations. By this, test pattern generation can be carried out in polynomial time. A technique to improve testability is presented. Experimental results show that a complete classification can be carried out very efficiently.

Boolean Satisfiability (SAT) solvers are popular engines used throughout the verification world. Bounded sequential problems such as bounded model checking and bounded sequential equivalence checking rely on fast and robust SAT solvers. In this work, we introduce a technique that improves the performance of the underlying SAT solver for bounded sequential problems by taking advantage of a design's don't care states. We develop cost effective methods of filtering, replicating and applying the don't care states to the original problem thus reducing the search space. Experiments demonstrate the effectiveness of the proposed method on ISCAS'89 benchmarks.

ASIC designs for future communication applications cannot be simulated exhaustively. Formal property checking is a powerful technology to overcome the limitations of current functional verification approaches. The paper reports on a large-scale experiment employing the CVE property checker for verifying the block-level functional correctness of a large ASIC. This new verification methodology achieves substantial quality and productivity gains. The two biggest advantages are: 1) coding and verification can be done in parallel; and 2) the whole state space of a test case will be verified in a single run. Formal property checking simplifies and shortens the functional verification of large-scale ASICs at least in the same order of magnitude as static timing analysis did for timing verification.

The complexity of integrated circuits is rapidly growing. This leads to more and more time and money spent on the test of these circuits. Besides minimizing the logic needed for a given function the testability of the resulting circuit becomes a major issue during synthesis. One way to synthesize a circuit for a given function is to directly convert the binary decision diagram (BDD) of that function into a circuit. It is known that optimizations of the BDD transfer to the derived circuit. Therefore in this paper we evaluate different optimization techniques for BDDs based on variable reordering with respect to the path delay fault testability of the resulting circuit. We show an optimization strategy that allows to compromise during synthesis between logic size and testability.

We present a technique to derive fully testable circuits under the stuck-at fault model (SAFM) and the path-delay fault model (PDFM). Starting from a function description as a binary decision diagram, the netlist is generated by a linear time mapping algorithm. Only one additional input and one inverter are needed to achieve 100% testable circuits under SAFM and PDFM. Experiments are given to show the advantages of the technique.

A new technique for synthesizing totally symmetric Boolean functions is presented that achieves complete robust path delay fault testability. BDDs are used for the synthesis step. Only one additional input and one inverter are needed to achieve 100% Path Delay Fault (PDF) testability. The size of the circuit is guaranteed to be at most quadratic in the number of inputs. The test vectors for any PDF can be generated in linear time. Experimental results underline the efficiency of the technique. In contrast to previous approaches, the technique can also be applied to multi-output functions.

We present a technique to derive fully testable circuits under the Stuck-At Fault Model (SAFM) and the Path-Delay Fault Model (PDFM). Starting from a function description as a Binary Decision Diagram (BDD) the netlist is generated by a linear time mapping algorithm. Only one additional input and one inverter are needed to achieve 100% testable circuits under SAFM and PDFM. Experiments are given to show the advantages of the the technique in comparison to previously presented methods.

Today up to 80% of the design costs for integrated circuits are due to verification. Verification tools guarantee completeness if equivalence of two designs or a property for a design is proven. In the other case, usually only one counter-example is produced. Then debugging has to be carried out to locate the design error. This paper investigates, how debugging can benefit from using more than one counter-example generated by the verification tool. The problem of finding useful counter-examples is theoretically analyzed and proven to be difficult. Heuristics are introduced and their quality is underlined by experimental results. Guidelines how to generate counter-examples are extracted from one of these heuristics.