Artificial Intelligence (AI) has demonstrated strong capabilities across various domains over the past decade. Edge and specifically mission-critical applications, such as automotive and aerospace, require both high performance and efficiency without compromises in security and reliability. This stems from tightly constrained power consumption, failures that can have catastrophic consequences and devices that may be physically accessible to malicious actors. AI algorithm deployment to hardware also presents significant barriers, requiring specialized knowledge and expensive development tools. The DI-EDAI project aims to offer a holistic approach for connecting high-level AI algorithms with hardware implementations while tackling the aforementioned issues. Unlike other approaches that address individual aspects of the AI deployment flow, we investigate solutions across multiple layers of the design stack. Through our work we develop efficient hardware, map AI algorithms to hardware while simultaneously ensuring security and reliability. Furthermore, we leverage AI-techniques to assist with Electronic Design Automation (EDA) workflows for design optimization, verification and implementation. Our open source approach aims to reduce entry barriers, promote transparency and education, and spark innovation. This paper presents the current state of the DI-EDAI project at midterm, highlighting our latest contributions, identifying limitations in existing state-of-the-art approaches, and outlining ongoing work to address these gaps.

Chip technologies are crucial for the digital transformation of industry and society. Machine Learning (ML) and Artificial Intelligence (AI) are increasingly shaping both daily life and industrial applications, with AI hardware playing a vital role in enabling efficient and scalable ML deployment. However, significant challenges remain in bridging the gap between ML algorithm development and hardware implementation, particularly for edge ML applications where efficiency, power constraints, and adaptability are critical. In such resource-constrained environments, hardware-software co-design becomes essential to achieve the necessary trade-offs between performance, energy efficiency, and system responsiveness. One of the key bottlenecks in ML hardware development is the lack of seamless integration between ML toolchains and electronic design automation (EDA) tools for hardware synthesis and mapping. Current solutions often require extensive manual optimization and costly proprietary software, limiting accessibility and innovation. Open-source tools can play a transformative role in democratizing ML hardware design, fostering collaboration, and addressing the growing shortage of skilled professionals. This paper covers key aspects of hardware-software co-design for ML systems, such as ML algorithms, hardware design, compiler technologies and system security, with a focus on open-source solutions. We highlight the critical need for open-source toolchains that connect ML model development with hardware synthesis and optimization and present solutions for custom hardware, as well as FPGA accelerators.

Many verification methods have been proposed to detect microarchitectural information leakage in response to the surge of security breaches in hardware designs. These sophisticated efforts have gone a long way toward preventing attackers from breaking the system’s confidentiality. However, each approach has its own set of weaknesses: it may not be scalable enough, exhaustive enough, flexible enough to meet changing requirements or fit well into existing verification flows. We propose FastPath, a hybrid verification methodology that combines the efficiency of simulation with the exhaustive nature of formal verification. FastPath employs a structural analysis framework to automate the method further. Our experimental results compare FastPath to a state-of-the-art formal approach, showing a significant reduction in manual effort while achieving the same level of exhaustive confidence. We also discovered and contributed a fix for a previously unknown leak of internal operands in cv32e40s, a RISC-V processor intended for security applications.

Chip technologies are crucial for the digital transformation of industry and society. Artificial Intelligence (AI) is playing an increasingly important role in both our daily lives and in industry. The development of advanced AI chip designs, essential for the successful deployment of AI, is of critical importance for innovation and competitiveness. However, challenges arise from the complexity of hardware development, expensive access to state-of-the-art design tools, and a global shortage of hardware experts. In addition to cost optimization, computational power, and energy consumption, security and trustworthiness are becoming increasingly important. This project aims to address these challenges in AI chip design by enabling efficient hardware development. We are developing a seamless transition between software-based AI model development and optimization, and efficient hardware implementation, while considering security, trustworthiness, and energy efficiency. An open-source approach plays a key role, facilitating access for small and medium-sized enterprises (SMEs) and expanding the community involved in AI chip design to help mitigate the shortage of skilled professionals.

Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) and/or parallelism between attacker and victim task execution. However, contradicting common intuitions, recent activities demonstrate that this threat is real even in microcontroller SoCs without such features. In this paper, we describe SoC-wide timing side channels previously neglected by security analysis and present a new formal method to close this gap. In a case study on the RISC-V Pulpissimo SoC, our method detected a vulnerability to a previously unknown attack variant that allows an attacker to obtain information about a victim's memory access behavior. After implementing a conservative fix, we were able to verify that the SoC is now secure w.r.t. the considered class of timing side channels.

The threat of hardware Trojans (HTs) in security-critical IPs like cryptographic accelerators poses severe security risks. The HT detection methods available today mostly rely on golden models and detailed circuit specifications. Often they are specific to certain HT payload types, making pre-silicon verification difficult and leading to security gaps. We propose a novel formal verification method for HT detection in non-interfering accelerators at the Register Transfer Level (RTL), employing standard formal property checking. Our method guarantees the exhaustive detection of any sequential HT independently of its payload behavior, including physical side channels. It does not require a golden model or a functional specification of the design. The experimental results demonstrate efficient and effective detection of all sequential HTs in accelerators available on Trust-Hub, including those with complex triggers and payloads.

Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts.

The increasing shift towards the RISC-V open-source instruction set architecture requires the development of new design techniques. In recent years, it has been demonstrated that RISC-V designs can be generated in a modular and scalable manner by utilizing metamodeling techniques. However, verifying these designs presents a significant challenge, because the verification must consider both Register Transfer Level (RTL) components and firmware components such as drivers. Furthermore, the interaction between firmware and hardware components is susceptible to various issues, including incorrect transaction sequences, synchronization problems, encoding mismatches, and reserved values. Traditionally, verifying the interaction between hardware and firmware requires simulation/emulation tools and verification engineers with expertise in both firmware and hardware. To overcome these challenges, this paper introduces an automated formal verification approach for FWHW Co-verification of peripherals such as timers and interrupt controllers, and their respective drivers in generated RISC-V designs. This verification process employs formal verification methods. This methodology enables the detection of bugs in both hardware and firmware because it consists of the verification of individual components that can be reused later in the integration process. By implementing this methodology in the early design stages, developers can identify and address potential issues more efficiently and avoid later corrections.

The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. The proposed methodology is based on an inductive property that enables scalability even to complex out-of-order cores. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. In addition, the paper discusses several techniques that can be used to make the verification process easier and faster. We demonstrate the feasibility of the proposed methodology through case studies on several open-source designs. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core. In addition to several hardware accelerators and in-order processors, our experiments also include RISC-V BOOM, a complex out-of-order processor, highlighting the scalability of the approach.

Spectre and Meltdown attacks proved Transient Execution Side Channels to be a notable challenge for designing secure microarchitectures. Various countermeasures against these threats were proposed on the electronic system level. However, addressing all possible attack scenarios requires the design and analysis of bit-and cycle-accurate implementations. We present a novel secure-by-construction RTL design methodology based on a new hardware protection framework underpinned by a generic control infrastructure that can be integrated into industry-grade microarchitectures. The methodology uses formal verification to systematically detect possible leakage paths and to customize the generic infrastructure accordingly for the design. We propose an iterative flow which semi-automatically leads to an RTL design that is guaranteed to be secure w.r.t. transient execution attacks. A case study for the methodology is conducted on BOOMv3, an open-source RISC-V processor with a deep out-of-order pipeline, and the resulting secure RTL design is benchmarked on an FPGA setup. Our design outperforms a design based on conservative countermeasures, improving the incurred overhead by$\boldsymbol{3}\times/\boldsymbol{4}\times$(depending on the threat model) while maintaining the same level of security.

Hardware (HW) security issues have been emerging at an alarming rate in recent years. Transient execution attacks, such as Spectre and Meltdown, in particular, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past. This papers addresses the need for a new approach to HW sign-off verification which guarantees the security of processors at the Register Transfer Level (RTL). To this end, we introduce a formal definition of security with respect to transient execution attacks, formulated as a HW property. We present a formal proof methodology based onUnique Program Execution Checking (UPEC)which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels. This is demonstrated by two new attack scenarios discovered in our experiments with UPEC. UPEC scales to a wide range of HW designs, including in-order processors (RocketChip), pipelines with out-of-order writeback (Ariane), and processors with deep out-of-order speculative execution (BOOM). To the best of our knowledge, UPEC is the first RTL verification technique that exhaustively covers transient execution side channels in processors of realistic complexity.

The importance of preventing microarchitectural timing side channels in security-critical applications has surged immensely over the last several years. Constant-time programming has emerged as a best-practice technique to prevent leaking out secret information through timing. It builds on the assumption that certain basic machine instructions execute timing-independently w.r.t. their input data. However, whether an instruction fulfills this data-independent timing criterion varies strongly from architecture to architecture.

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.

While semiconductors are becoming more efficient generation after generation, the continuous technology scaling leads to numerous reliability issues due, amongst others, to variations in transistors characteristics, manufacturing defects, component wear-out, or interference from external and internal sources. Induced bit flips and stuck-at-faults can lead to a system failure. Security-critical systems often use Physical Memory Protection (PMP) modules to enforce memory isolation. The standard loosely-coupled approach eases the implementation but creates overhead in area and performance, limiting the number of protected areas and their size. While delivering great support against malicious software and induced faults, better performance would benefit safety tasks by preventing the program from jumping into an undesired region and giving wrong outputs.We propose a novel model-driven approach to resolve these limitations by generating a tightly-coupled RISC-V PMP, which reduces the impact of run-time reconfiguration. We also discuss guidelines on configuring a PMP to minimize the overhead on performance and memory, and provide an area estimation for each possible PMP design instance. We formally verified a RISC-V Core with a PMP and evaluated its performance with the Dhrystone Benchmark. The presented architecture shows a performance gain of about 3 times against the standard implementation. Furthermore, we observed that adding the PMP feature to a RISC-V SoC led to a negligible performance loss of less than 0.1% per thousand PMP reconfigurations.

Safety-critical designs need to ensure reliable operations even under a hostile working environment with a certain degree of confidence. Continuous technology scaling has resulted in designs being more susceptible to the risk of failure. As a result, the safety requirements are constantly evolving and becoming more stringent. For validating and measuring the robustness of safety-critical designs, fault injection methods are employed within the design flows. To ensure safety requirements’ compliance, and at the same time to cope with the ever-increasing complexity of modern SoCs, the existing design flows become inadequate as the process is repetitive, time-tedious, and requires high manual efforts. In this paper, a fully automated, fast and accurate, fault emulation framework based on the FPGA platform is proposed that enables a high level of controllability and observability for fault injection. The approach uses model-driven engineering concepts and automates various fault injection campaigns, namely, statistical fault injection (SFI), direct fault injection (DFI), and exhaustive fault injection (EFI). A novel design architecture tailored for the FPGA platform is also proposed to improve the overall productivity of performing fault emulation. The proposed approach scales to a wide variety of RISC-V based CPU subsystems with varying complexity in size and features. The experimental results demonstrate a significant gain in the fault emulation performance by a factor of 2.75x to 47.57x when compared to the standard simulation-based fault injection methods.

The advent of IoT devices cleared the way for embedded systems to be used everywhere in daily life. These systems typically have very strict constraints on area and power consumption that are difficult, if not infeasible, to meet for commercial off-the-shelf (COTS) processors. At the same time, custom system designs are often not a viable option, due to price limits that force companies to keep design effort, cost and time to a minimum.This work proposes a highly automated method for a formal analysis of signal activity in a COTS processor during software (SW) execution. Our analysis provides a thorough understanding on the interaction between Hardware (HW) and SW with bit-level and clock cycle accuracy. Designers can use this knowledge to locate and exploit the identified behavioral patterns for a wide range of HW improvements. In this paper, we focus on qualifying switching activity by analyzing the controllability of signals. When applied to a SuperH-2 processor for different softwares, we were able to reduce its area by up to 69% and power by up to 56%. We demonstrate the scalability of this method on an industry-scale software system for IoT with about 1.7k lines of C code.

We propose a formal verification methodology to detect security-critical bugs in the hardware (HW) and in the hardware/firmware interface of SoCs. Our approach extends Unique Program Execution Checking (UPEC), originally proposed for detecting transient execution side channels, to also detect all functional design bugs that cause confidentiality violations, and to cover not only the processor but also its peripherals. The proposed methodology is particularly effective in capturing security vulnerabilities that are introduced based on cross-modular effects (integration and communication issues) or poorly understood hardware/firmware interaction. Such bugs are known to be hard to detect by previous methods.We demonstrate a compositional approach where vulnerabilities discovered by our method can be used to create restrictions for the software (SW). This supports design fixes not only at the HW but also at the SW level. We present experiments for the Pulpissimo platform (v4.0) where several security-critical bugs were identified (and confirmed), as well as for RocketChip.

The field of computer hardware stands at the verge of a revolution driven by recent breakthroughs in emerging nanodevices. “Nano Security” is a new Priority Program recently approved by DFG, the German Research Council. This initial-stage project initiative at the crossroads of nano-electronics and hardware-oriented security includes 11 projects with a total of 23 Principal Investigators from 18 German institutions. It considers the interplay between security and nano-electronics, focusing on a dichotomy which emerging nano-devices (and their architectural implications) have on system security. The projects within the Priority Program consider both: potential security threats and vulnerabilities stemming from novel nano-electronics, and innovative approaches to establishing and improving system security based on nano-electronics. This paper provides an overview of the Priority Program's overall philosophy and discusses the scientific objectives of its individual projects.

Resilience against hardware faults is a major concern for safety-critical embedded systems which has been addressed in several standards. These standards demand a systematic and thorough safety evaluation, especially for the highest safety levels. In order to provide the data for this evaluation, we propose a scalable and formal approach to fault propagation analysis for hardware/software systems. We consider soft errors by single event upsets (SEUs) which corrupt data in hardware registers and examine their effect on the high-level software. Our method identifies all faults of a given fault list that can have an effect on selected objects of the high-level software, such as the specified safety functions, and gives formal guarantees for other faults that do not do any harm.Scalability of our approach results from combining an analysis at the binary and hardware level with an analysis of the high-level source code using Abstract Interpretation. The result is a mapping between a fault in the hardware and affected locations in the source code. Effectiveness and scalability of this method are demonstrated on an industry-oriented software system with about 138 k lines of C code.

Transient execution attacks, such as Spectre and Meltdown, create a new and serious attack surface in modern processors. In spite of all countermeasures taken during recent years, the cycles of alarm and patch are ongoing and call for a better formal understanding of the threat and possible preventions.This paper introduces a formal definition of security with respect to transient execution attacks, formulated as a HW property. We present a formal method for security verification by HW property checking based on extending Unique Program Execution Checking (UPEC) to out-of-order processors. UPEC can be used to systematically detect all vulnerabilities to transient execution attacks, including vulnerabilities unknown so far. The feasibility of our approach is demonstrated at the example of the BOOM processor, which is a design with more than 650,000 state bits. In BOOM our approach detects a new, so far unknown vulnerability, called Spectre-STC, indicating that also single-threaded processors can be vulnerable to contention-based Spectre attacks.

The required manual effort and verification expertise are among the main hurdles for adopting formal verification in processor design flows. Developing a set of properties that fully covers all instruction behaviors is a laborious and challenging task. This paper proposes a highly automated and "complete" processor verification approach which requires considerably less manual effort and expertise compared to the state of the art.The proposed approach extends the S2QED approach to cover both single and multiple instruction bugs and ensures that a design is completely verified according to a well-defined criterion. This makes the approach robust against human errors. The properties are simple and can be automatically generated from an ISA model with small manual effort. Furthermore, unlike in conventional property checking, the verification engineer does not need to explicitly specify the processor's behavior in different special scenarios, such as stalling, exception, or speculation, since these scenarios are taken care of implicitly by the proposed computational model. The great promise of the approach is shown by an industrial case study with a 5-stage RISC-V processor.

This paper presents a semi-automatic methodology to create abstract driver models to be used as formal reference when developing the firmware for embedded device drivers. Our methodology extracts the behavior of driver software automatically as an abstract finite state machine. This replaces manually crafting these models from informal specifications, which is error-prone, laborious, and does not account for undocumented behavior. Our approach specifically targets untrusted driver software that is only available as binary code, for example as third-party IP, and for which the source code is unknown. Our extracted model is formally sound with respect to the implementation, while still being understandable by a human developer. Our experiments for industry-size driver software demonstrate that human-readable, sound, abstract driver models can be extracted from binary code in affordable run times and with small manual effort.

Code coverage analysis plays an important role in the software testing process. More recently, the remarkable effectiveness of coverage feedback has triggered a broad interest in feedback-guided fuzzing. In this work, we introduce bcov, a tool for binary-level coverage analysis. Our tool statically instruments x86-64 binaries in the ELF format without compiler support. We implement several techniques to improve efficiency and scale to large real-world software. First, we bring Agrawal’s probe pruning technique to binary-level instrumentation and effectively leverage its superblocks to reduce overhead. Second, we introduce sliced microexecution, a robust technique for jump table analysis which improves CFG precision and enables us to instrument jump table entries. Additionally, smaller instructions in x86-64 pose a challenge for inserting detours. To address this challenge, we aggressively exploit padding bytes and systematically host detours in neighboring basic blocks.

This paper presents a new Property-Driven Design (PDD) method that starts from an abstract system model and integrates formal property checking early into a top-down design methodology for register transfer level (RTL) hardware. In PDD the role of formal verification is not limited to “bug hunting” alone. Instead, the formal techniques are applied in such a way that a formal relationship is provided between the abstract system model and its concrete implementation at the RTL. In order to avoid the high efforts associated with verification by property checking the proposed PDD approach automatically generates abstract properties from a system-level description and later refines them along the design process. The advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional design flows with property checking. The main benefit of the proposed approach results from the fact that a formally sound system model is available together with the RTL design. Specifically, LTL properties proven on the abstract model also hold on the concrete implementation. This facilitates many complex analysis and verification tasks in today's design flows and contributes to emancipating system-level models from prototypes to golden design models. Several open-source and industrial case studies are reported that demonstrate the high potential of a PDD-based design paradigm.

Customizing embedded computing platforms to specific application domains often necessitates optimizing the firmware and/or the HW/SW interface under tight resource constraints. Such optimizations frequently alter the communication between the firmware and the peripheral devices, possibly compromising functional correctness of the input/output behavior of the embedded system. This paper proposes a formal HW/SW co-equivalence checking technique for verifying correct I/O behavior of peripherals under a modified firmware. We demonstrate the great promise of our approach on RTL implementations of several open-source peripherals. In our experiments we successfully prove or disprove correctness of firmware optimizations for an industrial driver software. In addition, we also found a subtle bug in one of the peripherals and several undocumented preconditions for correct device behavior.

Recent discovery of security attacks in advanced processors, known as Spectre and Meltdown, has resulted in high public alertness about security of hardware. The root cause of these attacks is information leakage across covert channels that reveal secret data without any explicit information flow between the secret and the attacker. Many sources believe that such covert channels are intrinsic to highly advanced processor architectures based on speculation and out-of-order execution, suggesting that such security risks can be avoided by staying away from high-end processors. This paper, however, shows that the problem is of wider scope: we present new classes of covert channel attacks which are possible in average-complexity processors with in-order pipelining, as they are mainstream in applications ranging from Internet-of-Things to Autonomous Systems. We present a new approach as a foundation for remedy against covert channels: while all previous attacks were found by clever thinking of human attackers, this paper presents a formal method called Unique Program Execution Checking which detects and locates vulnerabilities to covert channels systematically, including those to covert channels unknown so far.

We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several microcontroller core designs (~1,800 flip-flops, ~70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. (These additional bugs were also perhaps detected by the industrial verification flow.)3.Symbolic QED enables significant design productivity improvements: (a) 8X improved (i.e., reduced) verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED.

Small embedded devices are highly specialized plat forms that integrate several peripherals alongside the CPU core. Embedded devices extensively rely on Firmware (FW) to control and access the peripherals as well as other important functionality. This poses challenges to FW development since the FW must be adapted to each specific device configuration. Besides ensuring functional correctness to avoid errors and security vulnerabilities, an important design factor today is the control and adaptivity of a system with respect to non-functional properties, like for example application-specific timing budgets. Furthermore, optimizations of the FW and HW/SW interface play a very important role due to the tight resource constraints of small embedded devices. To satisfy these requirements new FW design methods are needed targeting FW generation, FW verification and FW optimization.This paper presents such new methods to enable an early, efficient and systematic FW design taking the underlying HW architecture into account. We use the RISC-V Instruction Set Architecture (ISA) as a case study to demonstrate our methods.

Formal techniques for the functional verification of System-on-Chip (SoC) hardware have matured significantly over the last years. They can penetrate deeply into a design to exhibit complex functional dependencies between various design components in terms of detailed logical and temporal relationships. They can also provide a well-defined formal relationship between an abstract system model of a design and its concrete implementation at the register-transfer level (RTL). This paper shows how such knowledge available from formal verification can be “condensed” into a database that stores all registers and flip-flops, at which time points they are actually relevant for the correct behavior of the design and when they are not. We show that the comprehensive information on temporary unobservabilities in the design can be of great value to reach two nonfunctional design goals that play a dominant role in many design flows: safety and low power consumption. This paper presents techniques to assess the effects of soft errors by single-event upsets (SEUs) with formal precision and to relate the results of the proposed analysis to an abstract system model. For example, our analysis can determine which soft errors may lead to a system “crash” and which are guaranteed not to cause any harm. For the application of the proposed approach in power optimization, this paper presents techniques for clock gating and power gating. For the examined designs, we observe a reduction of power consumption between 10% and 50% on top of the state-of-the-art commercial power synthesis.

Driven by the demand for highly customizable processor cores for IoT and related applications, there is a renewed interest in effective but low-cost techniques for verifying systems-on-chip (SoCs). This paper revisits the problem of processor verification and presents a radically different approach when compared to the state of the art. The proposed approach is highly automated and leverages recent progress in the field of post-silicon validation by the method of Quick Error Detection (QED) and Symbolic Quick Error Detection (SQED). In this paper, we modify SQED by incorporating a symbolic initial state in its BMC-based analysis and generalize the approach into the S2QED method. As a first advantage, S2QED can separate logic bugs from electrical bugs in QED-based postsilicon validation. Secondly, it also makes a strong contribution to pre-silicon verification by proving that the execution of each instruction is independent of its context in the program. The manual efforts for the proposed approach are orders of magnitude smaller than for conventional property checking. Our experimental results demonstrate the potential of S2QED using the Aquarius open-source processor example.

Today's applications for HW/SW-systems, such as the Internet-of-Things, often demand SoC architectures where sophisticated firmware is running on fairly simple processors. Designers face the challenge of meeting high requirements for these systems regarding their efficiency and dependability under severe cost constraints. Targeting such applications this paper presents a new technique to generate a joint computational model for the hardware and its firmware. Generation of our computational model is interleaved with techniques from WCET analysis so that clock-cycle accuracy of the resulting model is achieved. As an application of our approach, we present how to generate a fast, cycle-accurate RTL simulation model that can replace the processor and its firmware in the RTL system description. Our experimental results show an acceleration by an order of magnitude when applying standard cycle-accurate RTL simulation to our modified design.

We introduce goSAT, a fast and publicly available SMT solver for the theory of floating-point arithmetic. We build on the recently proposed XSat solver [1] which casts the satisfiability problem to a corresponding global optimization problem. Compared to XSat, goSAT is an integrated tool combining JIT compilation of SMT formulas and NLopt, a feature-rich mathematical optimization backend. We evaluate our tool using several optimization algorithms and compare it to XSat, Z3, and MathSat. Our evaluation demonstrates promising results.

In recent years early life failures have caused several product recalls in semiconductor and automotive industries associated with a loss of billions of dollars. They can be traced back to various root-causes. In embedded or cyber-physical systems, the interaction with the environment and the behavior of the hardware/software interface are hard to predict, which may lead to unforeseen failures. In addition to that, defects that have escaped manufacturing test or “weak” devices that cannot stand operational stress may for example cause unexpected hardware problems in the early life of a system. The special session focuses on the first aspect. The first contribution discusses how the interaction with the environment in cyber-physical systems can be appropriately modeled and tested. The second presentation then deals with a cross-layer approach identifying problems at the hardware/software interface which cannot be compensated by the application and must therefore be targeted by specific tests.

Embedded software is rapidly increasing in complexity. To cope with this, developers rely on third-party IPs to accelerate product delivery. However, IP source code might not be available which limits verifiability. This creates a particular challenge especially in safety-critical applications, e.g., automotive. Static Binary Analysis (SBA) is a promising technique to address such a challenge by providing engineers with the ability to reason about the actual instructions executed for all possible inputs. Disassembly is the fundamental first step for any SBA where assembly instructions are recovered from binary code. Correct disassembly, however, is challenging since data is mixed with code in binaries. Moreover, variable-size ISA, e.g., Thumb and TriCore, allow a single byte sequence to have multiple valid interpretations.

This paper discusses the possible role of formal verification techniques in system-level design flows. It is argued that the role of formal verification techniques should not be limited to “bug hunting” alone. Instead, formal technology should be applied in such a way that a formal relationship is provided between an abstract system model and its concrete implementation at the Register Transfer Level (RTL). In order to avoid the high efforts associated with verification by property checking this paper advocates for a top-down methodology where abstract properties are automatically generated from a system-level description and are later refined along the design process. One advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional property checking. Moreover, the proposed approach can be beneficial also when analyzing non-functional design targets. The paper demonstrates this for safety. We present experimental results that show how the effects of Single Event Upsets (SEUs) at the gate level of an SoC module can be related to safety requirements at the system's transaction level with formal precision.

Methods of Computer Algebra have shown to be useful when formally verifying data-centric hardware designs. This has been demonstrated especially for cases where complex arithmetic computations are tightly coupled with the system's control structures at the bit level. As a consequence of current design trends, however, more and more functionality that was traditionally implemented in hardware is now shifted into the low-level software of the system. Not only control functions but also more and more arithmetic operations and other data-centric functions are involved in this shift. Motivated by this observation, it is the goal of our work to extend the scope of computer-algebraic methods from hardware to low-level software. The paper develops how hardware-dependent software can be modeled algebraically so that efficient proof procedures are possible. Our results show that also in low-level software a computer-algebraic approach can have substantial advantages over state-of-the-art SMT solving.

This paper works towards a new design flow in which a design model at an architectural system level is refined into an RTL implementation in such a way that architectural model and RTL implementation stand in a well-defined formal relationship to each other. Functional properties valid at the system level are guaranteed to hold also in the concrete implementation without any additional verification efforts at the RTL. Based on the notion of path predicate abstraction (PPA) introduced in previous work, this paper contributes an "architectural modeling language (AML)" which formalizes the semantics of the architectural description level w.r.t. a PPA. The language is intended to be used only as an intermediate description automatically derived from standardized ESL languages such as SystemC when these descriptions are restricted to a mappable subset. Such an intermediate representation is needed to overcome the limitations of SystemC in precisely defining the semantics of the design model and its interfaces as well as to cope with the overwhelming expressive power of SystemC and the large syntactical diversity it allows. With an AML description of the architectural model as a starting point, the paper will show how properties in a standard language like SVA can be automatically generated that guarantee the correctness of the implementation when proven on the design after all refinement steps in the design and the property set have been completed.

This paper introduces a new property language for describing the behavior of low-level hardware-dependent software. The design of the language is motivated by the industrial success of property languages for hardware verification by simulation and formal techniques. The new language is constructed to concisely capture the timed behavior of the interactions between software and hardware by means of sequences. In this work we present how the proposed verification language can be used to perform formal verification based on a computational model called program netlist. We show how the sequence model of the language is synthesized and combined with the program netlist so that a unified formula for a decision procedure, e.g., a SAT solver, can be constructed. Furthermore, a method for coverage analysis of property sets is introduced. The coverage criterion we propose determines whether or not the property set completely describes the input/output functional behavior of a program. The paper presents a case study showing how to use the proposed property language in order to specify an industrial implementation of a LIN (Local Interconnect Network) bus driver.

In current practices of SoC design a trend can be observed to integrate more and more low-level software components into the hardware at different levels of granularity. The implementation of important control functions is frequently shifted from the SoC's hardware into its firmware. This calls for new methods for verification and test based on a joint analysis of hardware and software. While most techniques of software verification operate at a hardware-independent level, this paper elaborates on the possible merits of a hardware-dependent software view. It describes a model recently developed for formal HW/SW co-verification of embedded systems. New results are presented on how to model the interaction of hardware and software in a clock cycle-accurate way. The paper presents different application scenarios of the proposed models in SoC verification and outlines future perspectives in testing and the design of fault-resilient systems.

A formal methodology for system verification of system-on-chip (SoC) designs is proposed. It ensures that system-level models are created that are sound abstractions of the concrete implementations at the register transfer level (RTL). For each SoC module at the RTL, an abstract description is obtained by path predicate abstraction. Path predicate abstraction is introduced based on the notion of operational graph coloring. It is shown to what extent the proposed abstraction mechanism is related to the notion of a stuttering bisimulation employed in the field of theorem proving. The proposed methodology, however, does not rely on theorem proving but is entirely based on standard techniques of property checking. Path predicate abstraction leads to time-abstract system models that can be composed into abstract system models. We demonstrate the practical feasibility of our approach by two comprehensive industrial case studies.

This paper describes a method to generate a computational model for formal verification of hardware-dependent software in embedded systems. The computational model of the combined HW/SW system is a program netlist (PN) consisting of instruction cells connected in a directed acyclic graph that compactly represents all execution paths of the software. The model can be easily integrated into SAT-based verification environments such as those based on Bounded Model Checking (BMC). The proposed construction of the model, however, allows for an efficient reasoning of the SAT solver over entire execution paths. We demonstrate the efficiency of our approach by presenting experimental results from the formal verification of an industrial LIN (Local Interconnect Network) bus node, implemented as a software driver on a 32-bit RISC machine.

In formal verification, proof logging is a technique for automatically reviewing the reasoning steps of a proof engine by a separate tool. This is useful for enhancing the confidence in the prover's result, especially in the case of a positive answer when no counterexample exists. Mature proof logging techniques exist for single-theory provers. SMT solvers, however, combine several theories so that developing an unified proof logging technique is more challenging. This paper proposes an approach for logging the proofs of the SMT solver STABLE which is a prover combining SAT and computer algebra engines. We show how to translate the SAT proofs into algebraic forms (polynomials) and how to check the combined Boolean and word-level proofs using a separate computer algebra engine.

A new methodology for formal system verification of System-on-Chip (SoC) designs is proposed. It does not only ensure correctness of the system-level models but also of the concrete implementation at the Register-Transfer-Level (RTL). For each SoC module at the RTL an abstract description is obtained by path predicate abstraction. Since this leads to time-abstract system models the main challenge is to deal with the concurrency between the individual RTL components. We propose a compositional scheme describing the communication between SoC modules independently of their individual processing speed. The composed abstract system is modeled as an asynchronous composition and can be verified using the SPIN model checker. We demonstrate the practical feasibility of our approach by a comprehensive case study based on Infineon's FPI Bus.

Ensuring functional correctness of hardware and software is a bottleneck in every design process of Embedded Systems. This paper proposes an approach to formally verify low-level software in conjunction with the hardware. The proposed approach is based on Interval Property Checking (IPC) that has proved successful on large industrial hardware designs. In this paper, IPC is extended by a specific abstraction technique that makes it tractable for hardware/software co-verification on realistic industrial designs. In the proposed methodology sets of finite state sequences of the system are abstracted by interval properties. This allows us to handle long sequences of state transitions in the hardware as they occur when running programs. We demonstrate the feasibility of our approach using the example of an industrial LIN software running on a public domain microprocessor platform.

This paper presents a new SMT solver, STABLE, for formulas of the quantifier-free logic over fixed-sized bit vectors (QF-BV). The heart of STABLE is a computer-algebra-based engine which provides algorithms for simplifying arithmetic problems of an SMT instance prior to bit-blasting. As the primary application domain for STABLE we target an SMT-based property checking flow for System-on-Chip (SoC) designs. When verifying industrial data path modules we frequently encounter custom-designed arithmetic components specified at the logic level of the hardware description language being used. This results in SMT problems where arithmetic parts may include non-arithmetic constraints. STABLE includes a new technique for extracting arithmetic bit-level information for these non-arithmetic constraints. Thus, our algebraic engine can solve subproblems related to the entire arithmetic design component. STABLE was successfully evaluated in comparison with other state-of-the-art SMT solvers on a large collection of SMT formulas describing verification problems of industrial data path designs that include multiplication. In contrast to the other solvers STABLE was able to solve instances with bit-widths of up to 64 bits.

This paper proposes enhancements to SAT-based property checking with the goal to increase the spectrum of applications where a proof of unbounded validity of a safety property can be provided. For this purpose, invariants are computed by reachability analysis on an abstract model. The main idea of the paper consists in a BDD-based analysis of k-step-induction on the abstract model and its use to guide a step-wise refinement process of the initial abstraction. The property is then proven on a bounded model of the original design using the computed invariant. The new approach has been applied to formally verify industrial SoC modules. In our experiments, we consider particularly difficult verification tasks occurring in the context of protocol compliance verification using generic, transaction-style verification IPs. In our experiments, numerous properties are proven which either required substantial manual interaction in previous approaches, or cannot be proven at all by other methods available to us.

In this paper we describe a practical methodology to formally verify highly optimized, industrial multipliers. We define a multiplier description language which abstracts from low-level optimizations and which can model a wide range of common implementations at a structural and arithmetic level. The correctness of the created model is established by bit level transformations matching the model against a standard multiplication specification. The model is also translated into a gate netlist to be compared with the full-custom implementation of the multiplier by standard equivalence checking. The advantage of this approach is that we use a high level language to provide the correlation between structure and bit level arithmetic. This compares favorably with other approaches that have to spend considerable effort on extracting this information from highly optimized implementations. Our approach is easily portable and proved applicable to a wide variety of state-of-the-art industrial designs.

Arithmetic bit-level (ABL) normalization has been proven a viable approach to formal property checking of datapath designs. It is applicable where arithmetic components and sub-components can be identified at the register-transfer (RT) level of the design and the property. This paper extends the applicability of ABL normalization to cases where some of the arithmetic components are custom-designed entities, e.g., specified using Boolean equations or gates. We transform these entities into ABL building blocks using Reed-Muller expressions as an intermediate representation. We show how Boolean logic expressed in Reed-Muller form can be automatically transformed into ABL components so that such logic blocks can be treated together with the remaining ABL components in a subsequent normalization run. The approach is evaluated on a number of industrial designs generated by a commercial arithmetic module generator.

We propose a methodology to formally prove protocol compliance for communication blocks in System-on-Chip (SoC) designs. In this methodology, a set of operational properties is specified with respect to the states of a central finite state machine (FSM). This central FSM is called main FSM and controls the overall behavior of the design. In order to prove a set of compliance properties, we developed an approach that combines property checking on a bounded circuit model with an approximate reachability analysis. The property checker determines whether a property is valid for an arbitrary state of the design regardless of its reachability. In order to avoid false negatives, reachability constraints are added to the property, which are generated by an approximate FSM traversal algorithm. We show how the existence of a main FSM can be exploited systematically in the reachability analysis and how to partition both the transition relation and the state space such that the computational complexity is reduced drastically. This makes formal verification of protocol compliance tractable even for large designs with several thousand state variables. Our approach has been applied successfully to verify several industrial designs.

We propose a normalization technique for verifying arithmetic circuits in a bounded model-checking environment. Our technique operates on the arithmetic bit-level (ABL) description of the arithmetic circuit parts and property. The ABL description can easily be provided by the front-end of a register transfer level property checker. The proposed normalization greatly simplifies the SAT instances to be solved for arithmetic circuit verification. Our approach has been successfully applied to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.

We propose a normalization technique for verifying arithmetic circuits in a bounded model checking environment. Our technique operates on the arithmetic bit level (ABL) description of the arithmetic circuit parts and the property. The ABL description can easily be provided by the front-end of an RTL property checker. The proposed normalization greatly simplifies the SAT instances to be solved for arithmetic circuit verification. Our approach has been applied successfully to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.

In bounded model checking (BMC)-based verification flows lack of reachability constraints often leads to false negatives. At present, it is daily practice of a verification engineer to identify the missing reachability constraints by manually inspecting the design code and by analyzing counterexamples. This, unfortunately, requires a lot of effort and is prone to errors. We propose an algorithm to determine reachability constraints automatically. The proposed approach applies to a design style where the operation of the design is controlled by a main FSM which can easily be extracted from the RTL description of the circuit. The algorithm decomposes and analyzes the state space of the circuit by considering transitions of the main FSM. Experimental results show that the proposed method can considerably reduce the manual work of verification engineers.

We propose a new arithmetic reasoning calculus to speed up a SAT solver based on the Davis Putnam Longman Loveland (DPLL) procedure. It is based on an arithmetic bit level description of the arithmetic circuit parts and the property. This description can easily be provided by the front-end of an RTL property checker. The calculus yields significant speedup and more robustness on hard SAT instances derived from the formal verification of arithmetic circuits.

This paper proposes a new formalism for layout-driven optimization of datapaths. It is based on preserving an arithmetic bit level representation of the arithmetic circuit portions throughout various design stages. The arithmetic bit level description takes into account the arithmetic nature of the datapath and facilitates arithmetic reasoning to identify circuit transformations that are too complex to derive for Boolean reasoning. It is a bit-level representation so that it integrates well into standard design flows. Based on this representation, we developed an optimization algorithm for cycle time. It takes interconnect delay into account and can be applied at late design stages. A prototype has been integrated into a commercial EDA environment. For circuits implementing complex arithmetic expressions we achieved performance improvements of up to 32%.

One of the most severe shortcomings of currently available equivalence checkers is their inability to verify arithmetic circuits and multipliers, in particular. In this paper, we present a bit-level reverse-engineering technique that complements standard equivalence checking frameworks. We propose a Boolean mapping algorithm that extracts a network of half adders from the gate netlist of an addition circuit. Once the arithmetic bit-level representation of the circuit is obtained, equivalence checking can be performed using simple arithmetic operations. We have successfully applied the technique for the verification of a large number of multipliers of different architectures as well as more general arithmetic circuits, such as multiply/add units. The experimental results show the great promise of our approach.

This paper discusses a "structural" technique for traversing the state space of a finite state machine (FSM) and its application to equivalence checking of sequential circuits. The key ingredient to a state-space traversal is a data structure to represent state sets. In structural FSM, traversal-state sets are represented noncanonically and implicitly as gate netlists. First, we present an exact algorithm, which is based on an iterative expansion of the FSM into time frames and a network-decomposition procedure serving the same purpose as an existential quantification operation. Then, we discuss approximative algorithms for the application of structural FSM traversal to sequential equivalence checking. We theoretically analyze the properties of the exact as well as the approximative algorithms. Finally, we give details on the implementation of a sequential equivalence checker and present experimental results that demonstrate the effectiveness of the proposed approach for equivalence checking of optimized and retimed circuits.

Retiming is a widely investigated technique for performance optimization. It performs powerful modifications on a circuit netlist. However, often it is not clear whether the predicted performance improvement is still valid after placement has been performed. This paper presents a new retiming algorithm using a highly accurate timing model. It takes into account the effect of retiming on capacitive loads of single wires as well as fanout systems. Further, we propose the integration of retiming into a timing-driven standard cell placement environment. Retiming is used as an optimization technique throughout the whole placement process. The experimental results show the benefit of the proposed approach. In comparison with the conventional design flow based on the standard FEAS algorithm, our approach achieved an improvement in cycle time of up to 34% and 17% on the average.

In this paper, we show that under the constant delay model the placement problem is equivalent to minimizing a weighted sum of wire lengths. The weights can be efficiently computed once in advance and still accurately reflect the circuit area throughout the placement process. The existence of an efficient and accurate cost function allows us to directly optimize circuit area. This leads to better results compared to heuristic edge weight estimates or optimization for secondary criteria such as wire length. We leverage this property to improve a recursive partitioning based tool flow. We achieve area savings of 27% for some circuits and 15% on average. The use of the constant delay model additionally enables timing closure without iterations.

In this survey, we outline basic SAT- and ATPG- procedures as well as their applications in formal hardware verification. We attempt to give the reader a trace trough literature and provide a basic orientation concerning the problem formulations and known approaches in this active field of research.

Retiming is a widely investigated technique for performance optimization. It performs powerful modifications on a circuit netlist. However, often it is not clear whether the predicted performance improvement will still be valid after placement has been performed. This paper presents a new retiming algorithm using a highly accurate timing model taking into account the effect of retiming on capacitive loads of single wires as well as fanout systems. We propose the integration of retiming into a timing-driven standard cell placement environment based on simulated annealing. Retiming is used as an optimization technique throughout the whole placement process. The experimental results show the benefit of the proposed approach. In comparison with the conventional design flow based on standard FEAS (Leiserson and Saxe, J. VLSI and Computer Sys., pp. 41-67, 1983; and Algorithmica vol. 6, no 1, pp. 5-35, 1991.), our approach achieved an improvement in cycle time of up to 34% and 17% on the average.

One of the most severe shortcomings of currently available equivalence checkers is their inability to verify integer multipliers. In this paper, we present a bit level reverse-engineering technique that can be integrated into standard equivalence checking flows. We propose a Boolean mapping algorithm that extracts a network of half adders from the gate netlist of an addition circuit. Once the arithmetic bit level representation of the circuit is obtained, equivalence checking can be performed using simple arithmetic operations. Experimental results show the promise of our approach.

Channel routing is an NP-complete problem. Therefore, it is likely that there is no efficient algorithm solving this problem exactly.

Presents a new timing-driven approach for cell replication tailored to the practical needs of standard cell layout design. Cell replication methods have been studied extensively in the context of generic partitioning problems. However, until now, it has remained unclear what practical benefit can be obtained from this concept in a realistic environment for timing-driven layout synthesis. Therefore, this paper presents a timing-driven cell replication procedure, demonstrates its incorporation into a standard cell placement and routing tool, and examines its benefit on the final circuit performance in comparison with conventional gate or transistor sizing techniques. Furthermore, we demonstrate that cell replication can deteriorate the stuck-at fault testability of circuits and show that stuck-at redundancy elimination must be integrated into the placement procedure. Experimental results demonstrate the usefulness of the proposed methodology and suggest that cell replication should be an integral part of the physical design flow complementing traditional gate sizing techniques.

A new approach to optimize multilevel logic circuits is introduced. Given a multilevel circuit, the synthesis method optimizes its area while simultaneously enhancing its random pattern testability. The method is based on structural transformations at the gate level. New transformations involving EX-OR gates as well as Reed-Muller expansions have been introduced in the synthesis of multilevel circuits. This method is augmented with transformations that specifically enhance random-pattern testability while reducing the area. Testability enhancement is an integral part of our synthesis methodology. Experimental results show that the proposed methodology not only can achieve lower area than other similar tools, but that it achieves better testability compared to available testability enhancement tools such as tstfx. Specifically for ISCAS-85 benchmark circuits, it was observed that EX-OR gate-based transformations successfully contributed toward generating smaller circuits compared to other state-of-the-art logic optimization tools.

This paper presents a technique to determine prime implicants in multi-level combinational networks. The method is based on a graph representation of Boolean functions called AND/OR reasoning graphs. This representation follows from a search strategy to solve the satisfiability problem that is radically different from conventional search for this purpose (such as exhaustive simulation, backtracking, BDDs). The paper shows how to build AND/OR reasoning graphs for arbitrary combinational circuits and proves basic theoretical properties of the graphs. It will be demonstrated that AND/OR reasoning graphs allow us to naturally extend basic notions of two-level switching circuit theory to multi-level circuits. In particular, the notions of prime implicants and permissible prime implicants are defined for multi-level circuits and it is proved that AND/OR reasoning graphs represent all these implicants. Experimental results are shown for PLA factorization.

This paper proposes a technique for sequential logic equivalence checking by a structural fixed point iteration. Verification is performed by expanding the circuit into an iterative circuit array and by proving equivalence of each time frame by well-known combinational verification techniques. These exploit structural similarity between designs by local circuit transformations. Starting from the initial state, for each time frame the performed circuit transformations are stored (recorded) in an instruction queue. In subsequent time frames the instruction queue is re-used (played) and updated when necessary. At some point the instruction queue does not need to be modified any more and is valid in all subsequent time frames. Thus, a fixed point is reached and machine equivalence is proved by induction. Experimental results show the great promise of this approach to verify circuits after resynthesis and retiming.

This paper proposes a new approach to multilevel logic optimization based on automatic test pattern generation (ATPG). It shows that an ordinary test generator for single stuck-at faults can be used to perform arbitrary transformations in a combinational circuit and discusses how this approach relates to conventional multilevel minimization techniques based on Boolean division. Furthermore, effective heuristics are presented to decide what network manipulations are promising for minimizing the circuit. By identifying indirect implications between signals in the circuit, transformations can be derived which are "good" candidates for the minimization of the circuit. A main advantage of the proposed approach is that it operates directly on the structural netlist description of the circuit so that the technical consequences of the performed transformations can be evaluated in an easy way, permitting better control of the optimization process with respect to the specific goals of the designer. Therefore, the presented technique can serve as a basis for optimization techniques targeting nonconventional design goals. This paper only considers area minimization, and our experimental results show that the method presented is competitive with conventional technology-independent minimization techniques. For many benchmark circuits, our tool, the Hannover implication tool, based on learning (HANNIBAL) achieves the best minimization results published to date. Furthermore, the optimization approach presented is shown to be useful in formal verification.

A new logic optimization method of multi-level combinational CMOS circuits is presented, which minimizes both power as well as power dissipation per unit area. The method described here uses Boolean transformations which exploit implications at the gate-level, based on both controllability and observability relationships. New transformations which form the basis of our synthesis method are presented. The emphasis is on power consumption rather than on area. Experimental results demonstrate that circuits synthesized by our method consume less power with a comparable area than those synthesized by state-of-the-art tools.

A new methodology for formal logic verification of combinational circuits is presented. Specifically, a structural (logic network) approach is used, based on indirect implications derived by recursive learning. It is shown that implications can be used to capture similarity between designs. This is extended to formulate a hybrid approach, this structural (logic network) information is used to reduce the complexity of a subsequent functional method based on OBDDs. We demonstrate that OBDD-based verification can take great advantage of structural preprocessing in a synthesis environment where many small operations are performed that modify the circuit. The experimental results show that an effective combination can be achieved between memory efficient structural methods and powerful functional methods.

A new approach to optimize multi-level logic circuits is introduced. Given a multi-level circuit, the synthesis method optimizes its area, simultaneously enhancing its random pattern testability. The method is based on structural transformations at the gate level. New transformations involving EX-OR gates derived based on indirect implications by Recursive Learning have been introduced in the synthesis of multi-level circuits. This method is augmented with transformations that specifically enhance random-pattern testability while reducing the area. Testability enhancement is an integral part of our synthesis methodology. Experimental results show that the proposed methodology can not only realize lower area, but also achieves better testability compared to testability enhancement synthesis tools such as tstfx. Specifically for ISCAS-85 benchmark circuits, it was observed that EX-OR gate-based transformations can yield smaller circuits compared to state-of-the-art logic optimization tools like SIS and HANNIBAL.

Motivated by the problem of test pattern generation in digital circuits, this paper presents a novel technique called recursive learning that is able to perform a logic analysis on digital circuits. By recursively calling certain learning functions, it is possible to extract all logic dependencies between signals in a circuit and to perform precise implications for a given set of value assignments. This is of fundamental importance because it represents a new solution to the Boolean satisfiability problem. Thus, what we present is a new and uniform conceptual framework for a wide range of CAD problems including, but not limited to, test pattern generation, design verification, as well as logic optimization problems. Previous test generators for combinational and sequential circuits use a decision tree to systematically explore the search space when trying to generate a test vector. Recursive learning represents an attractive alternative. Using recursive learning with sufficient depth of recursion during the test generation process guarantees that implications are performed precisely; i.e., all necessary assignments for fault detection are identified at every stage of the algorithm so that no backtracks can occur. Consequently, no decision tree is needed to guarantee the completeness of the test generation algorithm. Recursive learning is not restricted to a particular logic alphabet and can be combined with most test generators for combinational and sequential circuits. Experimental results that demonstrate the efficiency of recursive learning are compared with the conventional branch-and-bound technique for test generation in combinational circuits. In particular, redundancy identification by recursive learning is demonstrated to be much more efficient than by previously reported techniques. In an important recent development, recursive learning has been shown to provide significant progress in design verification problems. Also importantly, recursive learning-based techniques have already been shown to be useful for logic optimization. Specifically, techniques based on recursive learning have already yielded better optimized circuits than the well known MIS-II.>

This paper introduces a new approach to logic verification of combinational circuits, which is based on recursive learning. In particular, the described method efficiently extracts equivalencies between internal nodes of the two circuits to be verified. We present a tool, HANNIBAL, which is very efficient for many practical verification problems where such internal equivalencies exist. The presented method can also be used to drastically accelerate other verification tools. Experimental results clearly show the efficiency of HANNIBAL. For example, HANNIBAL verifies the multiplier c6288 against the redundancy-free version c6288nr in only 48 s on a Sparc Workstation ELC.

An efficient technique for dynamic learning called oriented dynamic learning is proposed. Instead of learning being performed for almost all signals in the circuit, it is shown that it is possible to determine a subset of these signals to which all learning operations can be restricted. It is further shown that learning for this set of signals provides the same knowledge about the nonsolution areas in the decision trees as the dynamic learning of SOCRATES. High efficiency is achieved by limiting learning to certain learning lines that lie within a certain area of the circuit, called the active area. Experimental results are presented to show that oriented dynamic learning is far more efficient than dynamic learning in SOCRATES.>

Most test generators for combinational and sequential circuits use a branch and bound technique in order to systematically explore the search space when trying to generate a test vector. This paper presents an alternative method. Instead of using a decision tree to implicitly try all combinations of signal values for a given set of signals we use a learning routine which can be called recursively. Given enough recursions, it is guaranteed that we can identify all necessary assignments at a given stage of the algorithm. Our method is general in the sense that it can be combined with any logic alphabet and can be integrated in any FAN- based test generator for combinational circuits. Furthermore, recursive learning is equally applicable for test generation in sequential circuits and can even be used in hierarchical approaches. We show experimental results that demonstrate the attractiveness of our approach by comparing recursive learning with the conventional branch and bound technique for test generation in combinational circuits.