Despite decades of mitigation efforts, memory corruption bugs remain a dominant source of security vulnerabilities. CHERI, a capability-based architecture, directly targets this problem by replacing traditional pointers with Capabilities that encode bounds, permissions, and tamper-protection tags. However, CHERI represents a significant architectural intervention that impacts not only the processors core, but the entire Hardware/Software platform. System-level evaluation methods, such as Virtual Prototypes (VPs), have shown to be highly valuable for exploring, validating, and optimizing such complex Hardware/Software systems. This paper introduces the first open-source SystemC/TLMbased CHERI-enhanced RISC-V VP. The VP comes with support for Virtual Memory Management (VMM) and is capable of executing complex software stacks, such as the general purpose and memory-safe CheriBSD operating system. A verification using TestRIG demonstrates the VP’s robustness, passing 2.15 million test cases. A case study with CheriBSD and 10 representative, demanding benchmark workloads highlights the VP’s capability to simulate complex CHERI-enabled systems and to provide valuable insights for Hardware/Software co-design. The CHERI-enhanced VP, along with the Software used in our case study is available as open-source on GitHub.

In this paper, we enhance RVVTS, an open-source framework for testing RISC-V vector instructions, to enable comprehensive floating-point (FP) verification across various RISC-V simulators and FP libraries. Our enhanced RVVTS, referred to as FP-RVVTS, adds support for the RISC-V FP extensions (F, D, Zfh) through a novel context-free grammar specification with annotations, strengthened automatic single-instruction isolation, and improved failure cause analysis.In the experiments we show that FP-RVVTS generates FP test sets achieving over 95% functional coverage, reveals critical bugs in several RISC-V simulators, and, using isolated instructions, supports to narrow down the causes of failures.

Distributed (“satellite”) automotive radar systems employ multiple front and corner sensors whose raw-data fusion can improve angular resolution and imaging quality. In such central-processing architectures, however, single-chip radar Monolithic Microwave Integrated Circuits (MMICs) underutilize their integrated signal-processing resources, whereas transceiver MMICs still require a dedicated per-module microcontroller for configuration, diagnostics, and control tasks. This paper proposes Autonomous Radar Transceiver (ART), a transceiver-centric radar MMIC architecture that enables autonomous module-level operation without an external microcontroller. ART exploits otherwise idle non-sequencing windows of an on-chip RISC-V Sequencer (RVS) by time-partitioning its RISC-V CPU between (i) deterministic Frequency-Modulated Continuous-Wave (FMCW) sequencing and (ii) non-time-critical module control tasks. As a result, ART reduces satellite-radar module Bill of Materials (BOM) and integration complexity by consolidating control and sequencing into a single programmable chip while preserving sequencing determinism.

We present a highly automated, open-source RTL verification framework for the RISC-V Vector Extension (RVV) 1.0 that extends the open-source RVVTS framework by adding RTL support and a novel Automated Failure Categorization (AFC) stage for scalable result analysis. Using the most recent RTL of the silicon-proven Ara vector processor as DUT, we generate RVV test sets that encompass both positive and negative testing, and achieve over 96% functional coverage – significantly exceeding our evaluated baseline, which achieves only 11.04%. Our framework detects more than 82k deviations, automatically minimizes about 97% of them, and clusters observed failures into 16 distinct categories.

Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains such as formal verification, synthesis, and symbolic AI. Despite progress in solving techniques, less attention has been given to the infrastructure for constructing correct and efficient QBF encodings. For instance, it is often unclear whether two QBFs that encode the same problem in different ways yield the same solutions. Traditional QBF equivalence checking focuses only on free variables, yet in many cases, the quantified variables must also be considered. In this paper, we present QSOLE , the first fully automatic checker for solution-based QBF equivalence. Based on a recently introduced approach, QSOLE decomposes equivalence checks into smaller entailment computations and is capable of generating witnesses for detected inequivalences, which can be used to debug encodings. Furthermore, it allows for explicit exclusion of variables from equivalence checks enabling comparison of formulas using different local auxiliary variables.

Abstract The waveform viewer is one of the most important tools in a hardware engineer’s toolbox. It is the main interface used to track down design bugs found by simulation or formal verification. In this paper, we present Surfer, a modern waveform viewer designed to integrate with the broader hardware design ecosystem. It supports translation from bit vectors to semantically meaningful values, integration with simulation and verification tools, and lays the groundwork for interactive simulation in the open-source ecosystem.

TheInstruction Set Simulators (ISSs) used in Virtual Prototypes (VPs) are typically implemented as interpreters with the goal to be easy to understand, and fast to adapt and extend. However, the performance of instruction interpretation is very limited and the ever-increasing complexity of Hardware (HW) poses an increasing challenge to this approach. In this paper, we present optimization techniques for interpreter-based ISSs that significantly boost performance while preserving comprehensibility and adaptability. We consider the Risc-V Iss of an existing, SystemC-based open-source VP with extensive capabilities such as running Linux and interactive graphical applications. The optimization techniques feature a Dynamic Basic Block Cache (DBBCache) to accelerate ISS in-struction processing and a Load/Store Cache (LSCache) to speed up ISS load and store operations to and from memory. In our evaluation, we consider 12 Linux-based benchmark workloads and compare our optimizations to the original VP as well as to the very efficient official RISC-V reference simulator Spike maintained by RISC-V International. Overall, we achieve up to 406.97 Million Instructions per Second (MIPS) and a significant average performance increase, by a factor of 8.98 over the original VP and 1.65 over the Spike simulator. To showcase the retention of both comprehensibility and adaptability, we implement support for RISC-V half-precision floating-point extension (Zfh) in both the original and the optimized VP. A comparison of these implementations reveals no significant differences, ensuring that the stated qualities remain unaffected. The optimized VP including Zfh is available as open-source on GitHub.

Embedded systems play a crucial role in today’s Internet-of-Things (IoT) ecosystems. These systems can range from simple sensors to edge Artificial Intelligence (AI) solutions. However, their complex Hardware (HW)/Software (SW) interactions demand new analytical methodologies which encompass both the HW and the SW execution.In this work, we present a novel approach for early visualization of complex HW/SW interactions during SW development for embedded systems. Our approach traces the lifetime of HW and SW functions during the simulation of a Virtual Prototype (VP), which represents the HW while executing the SW. We dynamically instrument the execution of the VP at runtime such that neither the VP binary file nor the SW binary file has to be modified for tracing. The results are presented as a Function Lifetime Diagram (FLD) by storing the data into the Fast Transaction Recording (FTR) file format, which can be visualized, e.g. by the Surfer waveform viewer.To demonstrate the effectiveness of our approach, we first analyze the HW and SW interactions of a Micro-Electro-Mechanical System (MEMS) sensor. More specifically, the root causes of two already identified HW/SW interaction issues are analyzed. Second, the application flow of an edge AI application for recognizing handwritten digits on a touch display utilizing a pretrained Neural Network (NN) is analyzed. These experiments demonstrate that FLDs provide an effective abstraction to foster a deeper understanding of the embedded system behavior. An additional runtime evaluation reveals an approximately 1.9-fold runtime overhead, demonstrating that our instrumentation approach remains runtime-efficient even for larger IoT applications.

Modern applications increasingly rely on embedded systems that incorporate visual interfaces developed utilizing so-called embedded graphics libraries. Verifying these embedded graphics libraries is challenging due to hardware dependencies and the lack of reference outputs. The lack of reference outputs is tackled in Metamorphic Testing (MT) by constructing two Firmware (FW) versions with distinct implementations that maintain the same input-output relationships. These relations are known as Metamorphic Relations (MRs). However, the development of these MRs remains a tedious and challenging task.In this paper, we present a novel approach for generating MRs for MT of embedded graphics libraries using Large Language Models (LLMs). Because directly creating MRs with simple prompts is too complex for the LLM, we employ proven prompting strategies to develop our LLM-assisted MR pipeline. Strategies include role prompting, least-to-most prompting, zero-shot prompting, constraint-based prompting, and style prompting. In our experiments, we verify a widely used embedded graphics library. We compare our results with an existing manual approach and demonstrate that LLM-assisted MRs nearly doubles coverage and identifies additional bugs.

Transaction-level debugging in Virtual Prototypes (VPs) remains challenging due to the sheer number and intricate nature of interactions between software and hardware components. This paper presents ProtoLens, the first open-source tool for dynamic visualization of Transaction Level Modeling (TLM) transactions in SystemC-based VPs. Integrated with the open-source RISC-V VP++, ProtoLens provides an interactive web front-end that displays architecture-aware transaction flows in real-time. It captures transaction data via a lightweight extension of the TLM bus and enriches it with peripheral-specific views through user-defined modules, so-called Transaction View Modules (TVMs). Additionally, ProtoLens supports integration with software debuggers, allowing synchronized transaction inspection and control of the simulation flow. This enables developers to efficiently analyze issues such as incorrect memory mappings, unexpected peripheral behavior, and to better understand the overall system architecture.Two case studies highlight the capabilities of ProtoLens: one demonstrates how it complements classical debugging in a bare-metal software example, and the other showcases its ability to reconstruct real-time graphics output from a Linux-based game.

Abstract Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and—more recently—of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don’t cares for so-called Extended Atomic Blocks (EABs) and by Delayed Don’t Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).

Embedded graphics libraries are part of the firmware of embedded systems and provide complex functionalities optimized for specific hardware. After unit testing of embedded graphics libraries, integration testing is a significant challenge, in particular since the hardware is needed to obtain the output image as well as the inherent difficulty in defining the reference result. In this paper, we present a novel approach focusing on integration testing of embedded graphic libraries. We leverage Virtual Prototypes (VPs) and integrate them with Metamorphic Testing (MT). MT is a software testing technique that uncovers faults or issues in a system by exploring how its outputs change under predefined input transformations, without relying on explicit oracles or predetermined results. In combination with virtualizing the displays in VPs, we even eliminate the need for physical hardware. This allows us to develop a MT framework automating the verification process. In our evaluation, we demonstrate the effectiveness of our MT framework. On an extended RISC-V VP for the GD32V platform we found 15 distinct bugs for the widely used TFT eSPI embedded graphics library, confirming the strength our approach.

Taking a hardware design from concept to silicon is a long and complicated process, partly due to very long-running simulations. After modifying a Register Transfer Level (RTL) design, it is typically handed off to the simulator, which then simulates the full design for a given amount of time. If a bug is discovered, there is no way to adjust the design while still in the context of the simulation. Instead, all simulation results are thrown away, and the entire cycle must be restarted from the beginning.In this paper, we argue that it is worth breaking up this strict separation between design languages, analysis languages, verification languages, and simulators. We present virtual signals, a methodology to inject new logic into existing waveforms.Virtual signals are based on WAL, an open-source waveform analysis language, and can therefore use the capabilities of WAL for debugging, fixing, analyzing, and verifying a design. All this enables an interactive and fast response design-debug-verification cycle. To demonstrate the benefits of our methodology, we present a case-study in which we show how the technique improves debugging and design analysis.

This paper targets the optimization of circuit netlists by eliminating redundant gates under given external constraints. Typical examples for external constraints – which can be viewed as external don't cares – are restrictions on input operands, instruction subsets used by a processor for specific applications, or limited operation modes of an integrated IP block. Targeting external don't cares presents a challenge because the optimization problem changes from a completely specified Boolean function to a Boolean relation. We propose an optimization approach that utilizes formal verification methods. We demonstrate how to formulate Property Checking (PC) and Equivalence Checking (EC) problems to determine if a gate is redundant under given external constraints. Essentially, the validity of up to four rules must be checked per gate. We show that these checks can be solved concurrently, resulting in faster overall optimization. We have implemented our approach as the tool Formal SYNthesis (FSYN). FSYN utilizes open-source tools to scale the solving of formal instances with available hardware resources. We demonstrate that our approach can achieve substantial reductions in the number of gates for combinational circuits under given external constraints.

In this paper we introduce the first free- and open-source SystemC TLM based RISC-V Virtual Prototype (VP) with support for the RISC-V “V” Vector Extension (RVV) Version 1.0. After an introduction to RVV, we present the integration of RVV and its 600+ instructions into an existing VP leveraging code generation for over 20k Lines of Code (LoC). Moreover, we describe the verification of the resulting VP using the Instruction Sequence Generator (ISG) FORCE-RISCV and the Instruction Set Simulator (ISS) riscvOVPsim. Our case studies demonstrate the benefits of the RVV enhanced VP for system-level evaluation. We present non-vectorized and vectorized variants of two common algorithms which are executed on the VP with varying parameters. We show that by comparing the number of simulated execution cycles, we can derive valuable assessments for the design of RVV micro-architectures.

While the Hardware (HW) domain and the Software (SW) domain use the concept of coverage to measure the thoroughness of tests, there isn’t an established common metric that applies to both worlds. In this paper we make two major contributions: First, leveraging the abstraction of Virtual Prototypes (VPs), we unify HW/SW coverage by viewing the HW/SW system as a single model. This enables the measurement of structural HW/SW metrics like line, function, and branch coverage via a novel non-intrusive approach, where neither the VP (representing the HW) nor the SW requires any modification. Second, based on the unified HW/SW coverage, we introduce relation coverage. The innovation is that the user can define a relation between the frequency of executing lines in the SW and the execution count of corresponding lines of the HW model. This relation expresses expected behavior to be covered during testing. As a case study, we consider HW/SW testing of a Gyroscope sensor controlled by SW running on a RISC-V VP.

Caches are essential to achieve high performance in modern hardware designs as they bridge the performance gap between digital logic and memories. However, prior research for analyzing the cache performance does not support the designer during the cache implementation.In this paper, we present an extensible, automated, and flexible methodology for analyzing cache performance during HDL design. Our approach works by monitoring cache interfaces based on waveforms from simulators, formal tools, or logic analyzers. Both, the generic cache analysis algorithm and the analysis metrics are design agnostic and can be reused across designs and design configurations. We demonstrate that our methodology is applicable throughout all stages of the hardware development cycle from the first test, to debugging, all the way to multi-million cycle simulations.

Testing complex RISC-V extensions such as RISC-V Vector (RVV) with its 600+ highly configurable instructions is crucial. For this reason, test suites have been developed over the last years, including both hand-written and automatically generated tests. Although the process of running these tests is often highly automated, a significant portion of the work, namely the result analysis, has to be conducted manually after the run.

Starting points for design understanding and debugging of a Hardware Description Language (HDL) design are generated waveforms. However, waveform viewing is still a highly manual and tedious process, and unfortunately, there has been no progress for automating the analysis of waveforms. Therefore, we introduce the Waveform Analysis Language (WAL) in this paper. WAL allows to create and execute analysis programs on waveforms. We have realized WAL as a Domain Specific Language (DSL). This design choice has many advantages ranging from a natural expressiveness of a waveform analysis problem to providing an Intermediate Representation (IR) well-suited as a compilation target from other languages. We demonstrate the capabilities of WAL in four case studies, covering the analysis of hardware performance of different RISC-V processors, combined hardware/software profiling, the usage of WAL to analyze bus transactions, and the implementation of a new embedded DSL using WALs macro system.

The "operational approach" to software development is based on separation of problem-oriented and implementation-oriented concerns, and features executable specifications and transformational implementation. "Operational specification languages" are ...

In this paper, we present a novel approach for design understanding of processors. Our approach uses clustering techniques to identify datapath similarities based on control signal vectors. The resulting dendrogram captures the closeness of instructions wrt. their datapath and control in visual form. We demonstrate how our approach helps in design understanding of a RISC-V processor without reading the HDL code.

The time-to-market of a new product is one of its most crucial factors for success, therefore, reducing this time is of utter importance. However, this reduction must not come at the expense of a less thorough development process. This paper presents a compiler-driven approach for automatically analyzing metrics such as transaction delays or bus throughput on simulation waveforms of projects developed in the Spade Hardware Description Language (HDL). By utilizing the Spade compiler's knowledge about design internals, an automatic analysis of the waveforms created during simulation is possible using the Waveform Analysis Language (WAL). Analysis programs can be bundled with Spade projects or libraries, such that they are automatically detected by Spade and can be reused by other projects using simple annotations. We call these bundled WAL programs analysis passes, since they fit into the Spade workflow and provide thorough analysis at no additional cost to the users of these libraries. In a detailed description, we present how new analysis passes can be defined using the example of a data streaming interface. Additionally, we highlight the possibilities of analysis passes in two case studies, including Finite State Machine (FSM) and Wishbone protocol analysis.

Today, Virtual Prototypes (VPs) are heavily used to enable early software development and to accelerate the design process. The aim of this work is twofold: (i) enable the early development of interactive graphical applications running on Linux, and (ii) provide an easy-to-use and configurable solution for RISC-V. In this paper, we present GUI-VP Kit. GUI-VP Kit includes GUI-VP, a greatly extended and improved RISC-V VP, as well as configurations to build a runnable Linux environment, and input/output drivers that form the interface between peripherals and Linux applications. In our experiments employing GUI-VP Kit, we show that well-known X-applications can be executed in GUI-VP using a VNC network connection. Moreover, we demonstrate reasonable speed for a Linux port of a classic first-person 3D-game.

Starting points for design understanding and debugging are generated waveforms. However, waveform viewing is still a highly manual and tedious process, and unfortunately, there has been no progress for automating the analysis of waveforms. Therefore, we introduce the Waveform Analysis Language (WAL) in this paper. We have realized WAL as a Domain Specific Language (DSL). This design choice has many advantages ranging from a natural expressiveness of a waveform analysis problem to providing an Intermediate Representation (IR) well-suited as a compilation target from other languages. We evaluate WAL in two major case studies. This includes (i) a WAL-based communication analyzer reporting for example throughput or latency of AXI communication and (ii) the tracing of the instruction flow through the pipeline of a RISC-V processor as well as the extraction of software basic blocks via WAWK, which is based on the WAL-IR to make complex waveform analysis as easy as searching in text files.

In this paper, we demonstrate the use of the open-source domain specific language WAL to analyze performance metrics of RISC-V processors. The WAL programs calculate these metrics by evaluating the processors signals while "walking" over the simulation waveform (VCD). The presented WAL programs are flexible and generic, and can be easily adapted to different RISC-V cores.

Modular multipliers are the essential components in cryptography and Residue Number System (RNS) designs. Especially, 2n - 1 and 2n + 1 modular multipliers have gained more attention due to their regular structures and a wide variety of applications. However, there is no automated formal verification method to prove the correctness of these multipliers. As a result, bugs might remain undetected after the design phase.

In this paper we propose an effective approach for verification of real-world SystemC TLM peripherals using modern C++ symbolic execution tools. We designed a lightweight SystemC peripheral kernel that enables an efficient integration with the modern symbolic execution engine KLEE and acts as a drop-in replacement for the normal SystemC kernel on pre-processed TLM peripherals. The pre-processing step essentially replaces context switches in SystemC threads with normal function calls which can be handled by KLEE. Our experiments, using a publicly available RISC-V specific interrupt controller, demonstrate the scalability and bug hunting effectiveness of our approach.

Boosting hardware design productivity is a major plus of SpinalHDL, a Scala-based Hardware Description Language (HDL). SpinalHDL achieves this by providing object oriented programming, functional programming, and meta-hardware description finally enabling the generation of Verilog code. Despite all the advantages of SpinalHDL, verification is the biggest challenge here as well.In this paper, we bring Coverage-Guided Fuzzing (CGF), a well-established software testing technique, to the SpinalHDL design flow. We have implemented our approach SpinalFuzz on top of the fuzzer AFL++. We leverage Scala-features to automate as many tasks as possible and ease the integration of fuzzing in SpinalHDL. In the experiments we demonstrate the effectiveness of SpinalFuzz in comparison to Constrained Random Verification (CRV). For a wide range of SpinalHDL designs we show that SpinalFuzz outperforms CRV and reaches coverage-closure.

The open and royalty free nature as well as the extendable design of the RISC-V Instruction Set Architecture (ISA) has lead to a sprawling ecosystem of RISC-V software and hardware. One of the domains explored by the RISC-V community are processors with minimal area footprints. To reduce the area footprint to the minimum, typically performance is traded for a much more compact design. A promising approach to realizing very small RISC-V processors is to base them on a single instruction, such as SUBLEQ, and using a microcode layer. However, the minimalism of SUBLEQ makes writing correct microcode procedures challenging.In this paper, we target the formal verification of SUBLEQ microcode procedures. We present our verification framework and show that we can handle complex SUBLEQ procedures in practical times. In our experiments we consider a set of SUBLEQ procedures which implements the RV32I ISA and passes all official RISC-V compliance tests. However, based on our approach we found 9 intricate bugs in the SUBLEQ procedures.

In this paper, we propose a novel simulation-based cross-level approach for processor verification at the Register-Transfer Level (RTL). We leverage state-of-the-art coverage-guided fuzzing techniques from the software domain to generate processor-level input stimuli. An Instruction Set Simulator (ISS) is utilized as a reference model for the RTL processor under test in an efficient co-simulation setting. To further boost the fuzzing effectiveness, we devised custom mutation procedures tailored for the processor verification domain. Our experiments using the popular open-source RISC-V based VexRiscv processor demonstrate the effectiveness of our approach in finding intricate bugs at the processor level.

In this paper, we present RVVRadar, a framework to support the programmer over the four major steps of development, verification, measurement, and evaluation during the vectorization process of an algorithm. We demonstrate the advantages of RVVRadar for vectorization on several practical relevant algorithms. This includes in particular the widely-used libpng library where we vectorized all filter computations resulting in speedups of up to 5.43. We made RVVRadar as well as all benchmarks (including the RVV-based libpng) open source.

The formal verification of integer multipliers is one of the important but challenging problems in the verification community. Recently, the methods based on symbolic computer algebra (SCA) have shown very good results in comparison to all other existing proof techniques. However, when it comes to verification of huge and structurally complex multipliers, they completely fail as an explosion happens in the number of monomials. The reason for this explosion is the generation of redundant monomials known as vanishing monomials. This article introduces the SCA-based approach RevSCA-2.0 that combines reverse engineering and local vanishing removal to verify large and nontrivial multipliers. For our approach, we first come up with a theory for the origin of vanishing monomials, i.e., we prove that the gates/nodes where both outputs of half adders (HAs) converge are the origins of vanishing monomials. Then, we propose a dedicated reverse engineering technique to identify atomic blocks including HAs. The identified HAs are the basis for detecting converging cones and locally removing vanishing monomials, which finally results in a vanishing-free global backward rewriting. The efficiency of RevSCA-2.0 is demonstrated using an extensive set of multipliers with up to several million gates.

System-on-Chips (SoC) have imposed new yet stringent design specifications on the Radio Frequency (RF) subsystems. The Timed Data Flow (TDF) model of computation available in SystemC-AMS offers here a good trade-off between accuracy and simulation-speed at the system-level. However, one of the main challenges in system-level verification is the availability of reference models traditionally used to verify the correctness of the Design Under Verification (DUV). Recently, Metamorphic testing (MT) introduced a new verification perspective in the software domain to alleviate this problem. MT uncovers bugs just by using and relating test-cases.

Compliance testing for RISC-V is very important. Essentially, it ensures that compatibility is maintained between RISC-V implementations and the ever growing RISC-V ecosystem. Therefore, an official Compliance Test-suite (CT) is being actively developed. However, it is very difficult to achieve that all relevant functional behavior is comprehensively tested.

In this paper we build on Metamorphic Testing (MT), a verification technique which has been employed very successfully in the software domain. The core idea is to uncover bugs by relating consecutive executions of the program under test. Recently, MT has been applied successfully to the verification of Radio Frequency (RF) amplifiers at the system level as well. However, this is clearly not sufficient as the true complexity stems from Analog/Mixed-Signal (AMS) systems. In this paper, we go beyond pure analog systems, i.e. we expand MT to verify AMS systems. As a challenging AMS system, we consider an industrial PLL. We devise a set of eight generic Metamorphic Relations (MRs). Theses MRs allow to verify the PLL behavioral at the component level and at the system level. Therefore, we have created MRs considering analog-to-digital as well as digital-to-digital behavior. We found a critical bug in the industrial PLL which clearly demonstrates the quality and potential of MT for AMS verification.

In this paper we build on methods based on Symbolic Computer Algebra that have been applied successfully to multiplier verification and more recently to divider verification as well. We show that existing methods are not sufficient to verify optimized non-restoring dividers and we enhance those methods by a novel optimization method for polynomials w. r. t. satisfiability don't cares. The optimization is reduced to Integer Linear Programming (ILP). Our experimental results show that this method is the key for enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).

Verifying processors has been and still is a major challenge. Therefore, intensive research has led to advanced verification solutions ranging from ISS-based reference models, (cross-level) simulation down to formal verification at the RTL. During the verification of the processor implementation at the Instruction Set Architecture (ISA) level, test stimuli, i.e. test programs are needed. They are either created manually or with the aid of sophisticated test program generators. However, significant effort is required to produce thorough test programs.

Only a few trends have gained as much traction as Edge Computing and Neural Networks (NN). Both have the potential to radically change how technology influences us. However, since edge devices feature only very limited resources, the sheer amount of performance required by modern NNs limits their use on the edge. Especially, the conversion of Convolutional Neural Networks (CNN) into feasible on-chip designs remains a hard task. Currently, hand-crafted and most-often very heavy architectures have to be used as existing High-Level Synthesis (HLS) frameworks provide only inefficient solutions. In this paper, we introduce the Crossbar Neural Network (XbNN) architecture. Our architecture employs a novel approximate on-chip dot product encoding for the efficient synthesis of CNNs on hardware. This encoding embeds the weights used in CNNs into the hardware design itself, significantly reducing the required memory and computation time. In addition, we present a methodology for the automated conversion of traditional CNNs given in TensorFlow into accelerators on top of the XbNN architecture. To demonstrate the effectiveness of XbNN, we conduct experiments on a common CNN test dataset and analyze the accuracy and performance of the resulting XbNN accelerators. We show that XbNN (a) achieves similar accuracies compared to TensorFlow CNNs and (b) provides much better area and performance results in comparison to a state-of-the-art HLS flow.

Metamorphic Testing (MT) has been shown to be a very effective technique in the Software (SW) domain. MT does not require a reference model to compare against for testing but instead relies on Metamorphic Relations (MR) to derive the expected result from relationships between several calls to the function under test. An example of an MR is the expectation that the sum of an arbitrary list of integers remain unchanged regardless of it being sorted or reversed. Thus, a key requirement for applying MT effectively is availability of MRs specific to the domain at hand. In this paper, we propose MT to the domain of processor verification. As a case study, we consider the RISC-V Instruction Set Architecture (ISA) and provide MRs tailored for RISC-V For evaluation purposes, we propose an efficient on-the-fly MT framework that integrates the MRs with an Instruction Set Simulator (ISS). We measure the quality of those MRs by the number of mutations they kill, also referred to as mutation analysis. Our experiments demonstrate the effectiveness of the MRs to kill all mutations, which confirms our research question that MT is also a suitable technique for the domain of processor verification.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high simulation performance and at the same time yield accurate results, which are two conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-V ISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments, using bare-metal and operating system based benchmarks, demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.

Compliance testing for RISC-V is very important. Therefore, an official hand-written compliance test-suite is being actively developed. However, besides requiring significant manual effort, it focuses on positive testing (the implemented instructions work as expected) only and neglects negative testing (consider illegal instructions to also ensure that no additional/unexpected behavior is accidentally added). This leaves a large gap in compliance testing. In this paper we propose a fuzzing-based test-suite generation approach to close this gap. We found new bugs in several RISC-V simulators including riscvOVPsim from Imperas which is the official reference simulator for compliance testing.

Avoiding security vulnerabilities is very important for embedded systems. Dynamic Information Flow Tracking (DIFT) is a powerful technique to analyze SW with respect to security policies in order to protect the system against a broad range of security related exploits. However, existing DIFT approaches either do not exist for Virtual Prototypes (VPs) or fail to model complex hardware/software interactions.In this paper, we present a novel approach that enables early and accurate DIFT of binaries targeting embedded systems with custom peripherals. Leveraging the SystemC framework, our DIFT engine tracks accurate data flow information alongside the program execution to detect violations of security policies at run-time. We demonstrate the effectiveness and applicability of our approach by extensive experiments.

With the decline of Moore's Law, several post-CMOS technologies are currently under heavy consideration. Promising candidates can be found in the class of Field-coupled Nanocomputing (FCN) devices as they allow for highest processing performance with tremendously low energy dissipation. With upcoming design automation in this domain, the need for formal verification approaches arises. Unfortunately, FCN circuits come with certain domain-specific properties that render conventional methods for the verification non-applicable. In this paper, we investigate this issue and propose a verification approach for FCN circuits that addresses this problem. For the first time, this provides researchers and engineers with an automatic method that allows them to check whether an obtained FCN circuit design indeed implements the given/desired function. A prototype implementation demonstrates the applicability of the proposed approach.

RISC-V is gaining huge popularity in particular for embedded systems. Recently, a SystemC-based Virtual Prototype (VP) has been open sourced to lay the foundation for providing support for system-level use cases such as design space exploration, analysis of complex HW/SW interactions and power/timing/performance validation for RISC-V based systems.In this paper, we propose an efficient core timing model and integrate it into the VP core to enable fast and accurate performance evaluation for RISC-V based systems. As a case-study we provide a timing configuration matching the RISC-V HiFive1 board from SiFive. Our experiments demonstrate that our approach allows to obtain very accurate performance evaluation results while still retaining a high simulation performance.

Compliance testing for RISC-V is very important. Therefore, an official hand-written compliance test-suite is being actively developed. However, this requires significant manual effort in particular to achieve a high test coverage.In this paper we propose a test-suite specification mechanism in combination with a first set of instruction constraints and coverage requirements for the base RISC-V ISA. In addition, we present an automated method to generate a test-suite that satisfies the specification. Our evaluation demonstrates the effectiveness and potential of our method.

Formal verification methods have made huge progress over the last decades. However, proving the correctness of arithmetic circuits involving integer multipliers still drives the verification techniques to their limits. Recently, Symbolic Computer Algebra (SCA) methods have shown good results in the verification of both large and non-trivial multipliers. Their success is mainly based on (1) reverse engineering and identifying basic building blocks, (2) finding converging gate cones which start from the basic building blocks and (3) early removal of redundant terms (vanishing monomials) to avoid the blow-up during backward rewriting. Despite these important accomplishments, verifying optimized and technology-mapped multipliers is an almost unexplored area. This creates major barriers for industrial use as most of the designs are area and delay optimized. To overcome the barriers, we propose a novel SCA-method which supports the formal verification of a large variety of optimized multipliers. Our method takes advantage of a dynamic substitution ordering to avoid the monomial explosion during backward rewriting. Experimental results confirm the efficiency of our approach in the verification of a wide range of optimized multipliers including industrial benchmarks.

Power-awareness is now crucial in the design flow for System-on-Chip (SoC) development. The main objective of power-awareness is to implement a Power Management Strategy (PMS) for the SoC by generating a flexible, yet efficient Power Management Unit (PMU). As the cost of structural changes to a design increases in advanced stages of development, the PMU should be incorporated into the design as early as possible. At early stages, Virtual Prototype (VP) based design at the Electronic System Level (ESL) has become an industry accepted solution. However, existing methods focusing on generating a PMU at the ESL have several drawbacks, such as relying on designers' domain expertise, a low degree of automation and a lack of programmability. This paper introduces a novel approach that automatically generates a programmable PMU for a given VP at the ESL without the need for prior knowledge about the VP's structure and behavior. Our approach consists of three main phases: activity pattern extraction, power-aware analysis, and PMU generation. The programmability feature of the generated PMU enables designers to support various target applications. The efficiency and flexibility of the proposed approach are evaluated by the power consumption reduction enabled by the PMU within a real-world VP-based SoC platform.

Extensive processor verification at the Register-Transfer Level (RTL) is crucial to avoid bugs. Therefore, simulation-based approaches are prevalent but they require efficient test generation methods to achieve a thorough verification. In this paper we propose an efficient cross-level testing approach for processor verification targeting the RISC- V Instruction Set Architecture (ISA). We generate an endless instruction stream without restrictions on the generated instructions by evolving the instruction stream on-the-fly during simulation. An Instruction Set Simulator (ISS) is leveraged as reference model for the RTL core under test in a tightly coupled cross-level co-simulation setting. This enables a very efficient and comprehensive testing process. As a case-study we present results on the verification of the 32 bit pipelined RISC- V core of MINRES The Good Folk (TGF) Series Our approach has been very effective in finding several serious bugs.

For IoT devices the demand in faster execution and at the same time lower energy consumption is a pressing problem. A very promising solution are Application-Specific Instruction-set Processors (ASIPs). They make use of custom instructions, which are added to the processor, forming the Instruction-Set Extension (ISE) of a given Instruction Set Architecture (ISA). While the selection process for the ISE is already challenging, an incorrect ISE specification leads to severe problems: errors and security vulnerabilities go undetected in the first formalization and in the worst case show up ultimately in the final implementation. In this paper, we propose an early verification approach for ISE specifications. Our novel approach is based on two ingredients: (i) Virtual Prototypes (VPs) to enable a rapid creation of an executable specification for the ISE; and (ii) Deep Reinforcement Learning (DRL) to search for ISE programs which violate the ISE specification intent. As case study we consider extensions of the RISC-V base ISA. We demonstrate the effectiveness of our approach for finding functional bugs in the executable specification of the ISE as well as specification gaps in the ISE leading to information leakage.

Extensive verification of embedded SW is very important to avoid errors and security vulnerabilities. Therefore, mainly simulation-based methods are employed that leverage Virtual Prototypes (VPs) for SW execution early in the design flow. VPs are essentially abstract models of the entire HW platform including peripherals. They are predominantly created in SystemC. However, a comprehensive simulation-based verification requires integration of sophisticated test generation techniques.

Recently, Virtual Prototypes (VPs) were introduced for the emerging RISC-V Instruction Set Architecture (ISA) and become an important part of the growing RISC-V ecosystem. A central component of the VP is the Instruction Set Simulator (ISS). VPs should provide a high performance and at the same time yield accurate results, which are conflicting requirements. To tackle this problem, we present an efficient VP-based adaptive simulation that is tailored for the RISC-VISA and allows to seamlessly switch the accuracy setting in the ISS at runtime. This enables to selectively simulate the application as fast as possible and as accurate as necessary. In this paper we focus on the performance impact of different accuracy settings and leave the evaluation of accuracy results for future work. Our RISC-V experiments demonstrate that up-to 543x speed-up is possible with a JIT-based setting in the ISS.

Virtual Prototypes (VPs) are becoming increasingly attractive for the early analysis of SoC power management, which is nowadays mostly implemented in firmware (FW). Power and timing constraints can be monitored and validated by executing a set of test-cases in a power-aware FW/VP co-simulation. In this context, cross coverage of power states is an effective but challenging quality metric. This paper proposes a novel coverage-driven approach to automatically generate test-cases maximizing this cross coverage. In particular, we integrate a coverage-loop that successively refines the generation process based on previous results. We demonstrate our approach on a LEON3-based VP.

Field-coupled Nanocomputing (FCN) technologies are considered as a solution to overcome physical boundaries of conventional CMOS approaches. But despite ground breaking advances regarding their physical implementation as e.g. Quantum-dot Cellular Automata (QCA), Nanomagnet Logic (NML), and many more, there is an unsettling lack of methods for large-scale design automation of FCN circuits. In fact, design automation for this class of technologies still is in its infancy - heavily relying either on manual labor or automatic methods which are applicable for rather small functionality only. This work presents a design method which - for the first time - allows for the scalable design of FCN circuits that satisfy dedicated constraints of these technologies. The proposed scheme is capable of handling around 40000 gates within seconds while the current state-of-the-art takes hours to handle around 20 gates. This is confirmed by experimental results on the layout level for various established benchmarks libraries.

Nowadays electronic systems are small yet powerful and embedded into their environment. They are adapting to changes and often operate autonomously. These systems have reached a level of complexity that opens up new application areas, like autonomous driving or self-learning robotics, but at the same time strains the existing design flows in system development. For two concrete examples we show the importance of ensuring the correctness: verification of robotic plans, and verified partial reconfiguration as part of a reconfiguration-based countermeasure against side-channel attacks.

Extensive testing of IoT SW is very important to prevent errors and security vulnerabilities. In the SW domain the automated concolic testing technique has been shown very effective.

In recent years, formal methods based on Symbolic Computer Algebra (SCA) have shown very good results in verification of integer multipliers. The success is based on removing redundant terms (vanishing monomials) early which allows to avoid the explosion in the number of monomials during backward rewriting. However, the SCA approaches still suffer from two major problems: (1) high dependence on the detection of Half Adders (HAs) realized as AND-XOR gates in the multiplier netlist, and (2) extremely large search space for finding the source of the vanishing monomials. As a consequence, if the multiplier consists of dirty logic, i.e. for instance using non-standard libraries or logic optimization, the existing SCA methods are completely blind on the resulting polynomials, and their techniques for effective division fail.

Approximate Computing (AC) is a design paradigm that makes use of the error tolerance inherited by many applications. The goal of AC is to trade off accuracy for performance in terms of computation time, energy consumption and/or hardware complexity.In the field of circuit design for AC, error-metrics are used to express the degree of approximation. Evaluating these error-metrics is a key challenge. Several approaches exist, however, to this day not all relevant metrics can be evaluated with formal methods. Recently, Symbolic Computer Algebra (SCA) has been used to evaluate error-metrics during approximate hardware generation. In this paper, we generalize the idea to use SCA and propose a methodology which is suitable for formal evaluation of all established error-metrics. This approach can be divided into three stages: 1) Determine the remainder of the AC circuit wrt. the specification using SCA, 2) build an Algebraic Decision Diagram (ADD) to represent the remainder and 3) evaluate each error-metric by a tailored ADD traversal algorithm. In the experiments, we apply our algorithms to a large and well-known benchmark set.

Internet-of-Things (IoT) devices have significantly increased the need for high quality Analog Mixed Signal (AMS) System-on-Chips (SoC). Virtual Prototyping (VP) can be utilized for an early design verification. The Timed Data Flow (TDF) model of computation available in SystemC-AMS offers here a good trade-off between accuracy and simulation-speed at the system-level. One of the main challenges in system-level verification of AMS design is to achieve full path coverage. In the software domain Data Flow Testing (DFT) has demonstrated to be a powerful testing strategy in this regard. In this paper we introduce a DFT approach for SystemC-AMS TDF models based on two major contributions: First, we develop a set of SystemC-AMS TDF models specific coverage criteria for DFT. This requires to consider the SystemC-AMS semantics of signal flow. Second, we explain how to automatically compute the data flow coverage result for given TDF models using a combination of static and dynamic analysis techniques. Our experimental results on real-world AMS VPs demonstrate the applicability and efficacy of our approach.

Verification of Instruction Set Simulators (ISSs) is crucial. Predominantly simulation-based approaches are used. They require a comprehensive testset to ensure a thorough verification.We propose a novel coverage-guided fuzzing (CGF) approach to improve the testcase generation process. In addition to code coverage we integrate functional coverage and a custom mutation procedure tailored for ISS verification. As a case-study we apply our approach on a set of three publicly available RISC-V ISSs. We found several new errors, including one error in the official RISC-V reference simulator Spike.

High-level Synthesis (HLS) is being increasingly adopted as a mean to raise design productivity. HLS designs, which can be automatically translated into RTL, are typically written in SystemC at a more abstract level. Hardware Trojan attacks and countermeasures, while well-known and well-researched for RTL and below, have been only recently considered for HLS. The paper makes a contribution to this emerging research area by proposing a novel detection approach for Hardware Trojans in SystemC HLS designs. The proposed approach is based on coverage-guided fuzzing, a new promising idea from software (security) testing research. The efficiency of the approach in identifying stealthy behavior is demonstrated on a set of open-source benchmarks.

In this paper, we propose the first approach for verifying plans of cognition-enabled autonomous robots that perform everyday manipulation activities in human environments. Our methodology is based on the new Intermediate Plan Verification Language (IPVL) which is used to represent plans, environments, and robot belief states in one joint formal model. We devise a symbolic execution engine for IPVL and show the effectiveness of our overall verification methodology in a case study.

Within the last decades, tremendous research work has been carried out on the development of software-based algorithms to solve the Boolean Satisfiability Problem. These SAT-solvers have then been heavily orchestrated for addressing complex computational tasks like the verification of circuits. In this field, most of the applied techniques focused only on the design phase of the circuit. Due to this fact, new approaches have been published in the literature solely focusing on online verification as well as self-verification. These kind of solutions strictly require Hardware (HW) SAT-solvers that can be integrated into a system while introducing only low hardware overhead and still providing high flexibility. By following these observations, this work presents SAT-Hard: In contrast to the state-of-the-art, SAT-Hard takes advantage of learning techniques to support features like clause learning and non-chronological backtracking, and combines them within a lightweight and standalone HW device. By this, a run-time speed-up of 2,000x can be achieved. Furthermore, the experimental evaluation clearly demonstrates that those complex problems can be solved in less than 20 seconds. Particularly due to its compactness, SAT-Hard is suitable for self-verification that enables the continuous verification of an integrated system during its lifetime.

In this paper we propose the first functional coverage-driven characterization approach as a systematic solution for the class of Radio Frequency (RF) amplifiers. We elevate the main concepts of digital functional coverage to the context of SystemC AMS in particular, and system-level simulations in general. To enable AMS functional coverage-driven characterization, we introduce two coverage refinement parameters on input and output side, to systematically generate input stimuli and capture specifications. At the heart of the approach is the coverage analysis which measures the functional coverage of the DUV and provides clear feedback to reach coverage closure. We provide a case study using an industrial RF transmitter and receiver model to demonstrate the applicability and efficacy of our approach.

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.

The exponential increase in functionality of System-on-Chips (SoCs) and reduced Time-to-Market (TTM) requirements have significantly altered the typical design and verification flow. Virtual Prototyping (VP) at the Electronic System Level (ESL) using SystemC and its Transaction Level Modeling (TLM) framework is an industry-accepted solution. VP design exploration, review, debugging, and integration of ever changing functional requirements can be made faster with the help of design understanding and visualization methods. Hence, in this paper, we propose a fully automated structural, and behavioral analysis approach for visualization of ESL VPs including TLM-2.0 VPs. At the heart of the analysis is a hybrid approach which uses static and dynamic methods to extract structural and behavioral information of the VP. Afterwards, the extracted information is translated into structural and graphical representations such as UML diagrams (specifying TLM-2.0 transactions' protocols), and XML format (describing designs' structure). Experimental results including a real-world VP shows the effectiveness of our approach.

Field-coupled Nanocomputing (FCN) technologies provide an alternative to conventional CMOS-based computation technologies and are characterized by intriguingly low-energy dissipation. Accordingly, their design received significant attention in the recent past. FCN circuit implementations like Quantum-dot Cellular Automata (QCA) or Nanomagnet Logic (NML) have already been built in labs and basic operations such as inverters, Majority, AND, OR, and so on, are already available. The design problem basically boils down to the question of how to place basic operations and route their connections so that the desired function results while, at the same time, further constraints (related to timing, clocking, path lengths, etc.) are satisfied. While several solutions for this problem have been proposed, interestingly no clear understanding about the complexity of the underlying task exists thus far. In this research note, we consider this problem and eventually prove that placement and routing for tile-based FCN circuits is NP -complete. By this, we provide a theoretical foundation for the further development of corresponding design methods.

Formal verification of high-level SystemC designs is an important and challenging problem. One has to deal with the full complexity of C++ to extract a suitable formal model (front-end problem) and then, with large cyclic state spaces defined by symbolic inputs and concurrent processes. This paper describes a scalable and efficient stateful symbolic simulation approach for SystemC that combines state subsumption reduction (SSR) with partial order reduction (POR) and symbolic execution (SymEx) under the SystemC simulation semantics. While the SymEx+POR combination provides basic capabilities to efficiently explore the state space, SSR prevents revisiting symbolic states and therefore makes the verification complete. The approach has been implemented on top of an intermediate verification language for SystemC to address the front-end problem. The scalability and efficiency of the implemented verifier is demonstrated using an extensive set of experiments.

A wide range of applications significantly benefit from the Approximate Computing (AC) paradigm in terms of speed or power reduction. AC achieves this by tolerating errors in the design. These errors are introduced into the design either manually by the designer or by approximate synthesis approaches. From here, the standard design flow is taken. Hence, the manufactured AC chip is eventually tested for production errors using well established fault models. To be precise, if the test for a test pattern fails, the AC chip is sorted out. However, from a general perspective this procedure results in throwing away chips which are perfectly fine taking into account that the considered fault (i.e. physical defect that leads to the error) can still be tolerated because of approximation. This can lead to a significant amount of yield loss. In this paper, we present an approximation-aware test methodology which can be easily integrated into the regular test flow. It is based on a pre-process to identify approximation-redundant faults. By this, we remove all potential faults that no longer need to be tested because they can be tolerated under the given error metric. Our experimental results and case studies on a wide variety of benchmark circuits show a significant potential for yield improvement.

Many applications are inherently error tolerant. Approximate Computing is an emerging design paradigm, which gives the opportunity to make use of this error tolerance, by trading off accuracy for performance. The behavior of a circuit can be defined at an arithmetic level, by describing the input and output relation as a polynomial. Symbolic Computer Algebra (SCA) has been employed to verify that a given circuit netlist matches the behavior specified at the arithmetic level. In this paper, we present a method that relaxes the exactness requirement of the implementation. We propose a heuristic method to generate an approximation for a given netlist and use SCA to ensure that the result is within application-specific bounds for given error-metrics. In addition, our approach allows for automatic generation of approximate hardware wrt. application-specific input probabilities. To the best of our knowledge taking input probabilities, which are known for many practical applications, into account has not been considered before. We employ the proposed approach to generate approximate adders and show that the results outperform state-of-the-art, handcrafted approximate hardware.

Analog-Mixed Signal (AMS) circuits have become increasingly important for today's SoCs. The Timed Data Flow (TDF) model of computation available in SystemC-AMS offers here a good tradeoff between accuracy and simulation-speed at the system-level. One of the main challenges in system-level verification is the quality of the testbench. In this paper, we present a testbench qualification approach for SystemC-AMS TDF models. Our contribution is twofold: First, we propose specific mutation models for the class of filters implemented as TDF models. This requires to analyze the Laplace transfer function of the filter design. Second, we present the mutation-based qualification approach based on the proposed specific mutations as well as standard behavioral mutations. This allows to find serious quality issues in the testbench. Our experimental results for a real-world AMS system demonstrate the applicability and efficacy of our approach.

An ESL design flow starts with a TLM description, which is thoroughly verified and then refined to a RTL description in subsequent steps. The properties used for TLM verification are refined alongside the TLM description to serve as starting point for RTL property checking. However, a manual transformation of properties from TLM to RTL is error prone and time consuming. Therefore, in this paper we propose a fully automated TLM-to-RTL property refinement based on a symbolic analysis of transactors. We demonstrate the applicability of our property refinement approach using a case study.

There is a growing need for error-resilient software that can tolerate hardware faults as well as for new resilience evaluation techniques. For the latter, a promising direction is to apply formal techniques in fault injection-based evaluations to improve the coverage of evaluation results. Building on the recent development of Software-implemented Fault Injection (SWiFI) techniques on compiler's intermediate code, this paper proposes a novel resilience evaluation framework combining LLVM-based SWiFI and SMT-based symbolic execution. This novel combination offers significant advantages over state-of-the-art approaches with respect to accuracy and coverage.

Quantum-dot Cellular Automata (QCA) are an emerging computation technology in which basic states are represented by nanosize particles and logic operations are conducted through corresponding effects such as Coulomb interaction. This allows to overcome physical boundaries of conventional solutions such as CMOS and, hence, constitutes a promising direction for future computing devices. Despite these promises, however, the development of (automatic) design methods for QCAs is still in its infancy. In fact, QCA circuits are mainly designed manually thus far and only few heuristics are available. This frequently leads to unsatisfactory results and generally makes it hard to evaluate the quality of respective QCA designs. In this work, we propose an exact solution for the design of QCA circuits that can be configured e.g. to generate circuits that satisfy certain design objectives and/or physical constraints. For the first time, this allows for design exploration of QCA circuits. Experimental evaluations and case studies demonstrate the benefit of the proposed solution.

The increased importance of power consumption as a design factor is now undeniable. Power aware design flows are increasingly targeting high abstraction levels (e.g. ESL), where optimization gains are bigger. The designers are thus required to define the power intent already at these levels. Here the major challenge is to perform power domain partitioning. However, this is a fully manual step based on reading and understanding the system specification, and it has to be performed before the Virtual Prototype (VP) is built. This paper presents an approach to aid architects in specifying power intent by suggesting coarse-grained power domain partitioning schemes, as the VP is built. The approach starts with structural and behavioral information being extracted from the system specification using Natural Language Processing (NLP) techniques. Then, a semantic network map is created which depicts the hierarchical structure and the abstract block level dependencies that can be used as a foundation for the VP. Finally, a partitioning scheme is derived from the application of an extendable set of analytic rules. Experimental results on an encoding system demonstrate the applicability and efficacy of the proposed approach.

Approximate computing is an emerging design paradigm for trading off computational accuracy for computational effort. Due to their inherited error resilience many applications significantly benefit from approximate computing. To realize approximation, dedicated approximate circuits have been developed and provide a solid foundation for energy and time efficient computing. However, when it comes to the design and integration of the approximate HW, complex error analysis is required to determine the effect of the error with respect to application specific error norms. This frequently leads to sub-optimal results. In this work, we propose to reverse the typical design flow for approximate HW and demonstrate the new flow for a first application: LU-Factorization, which is one of the most basic and most popular numerical algorithm known. The general idea of the reversed flow for approximate HW design is to start with the application and determine the required computational accuracy such that the computational error of the result is below the application specific error bound. This allows us to push the approximate HW to its limits, while guaranteeing that the result is correct by construction wrt. the requirements. The effectiveness of our approach for LU-Factorization is shown on a well-known and large set of benchmarks.

Quantum-Dot Cellular Automata (QCA) are an emerging nanotechnology with remarkable performance and energy efficiency. Computation and information transfer in QCA is based on field forces rather than electric currents. As a consequence, new strategies are required for design automation approaches in order to cope with the arising challenges. One of these challenges rises from the fact that QCA is a planar technology. That means, logic gates as well as interconnection elements are mostly located in the same layer. Hence, it is expected that interconnections have higher influence on the final design costs than in conventional integrated technologies. For the first time, this paper presents an extensive study on the quantification of this impact. Therefore, we consider the entire design flow for QCA circuits from the initial synthesis (using different synthesis approaches) to the corresponding placement on a QCA grid. Then, we characterize the respectively obtained QCA circuits in terms of area, delay and energy costs. The obtained results indicate that the impact of interconnections in QCA is indeed substantial. Design costs including or not including interconnections differ by several orders of magnitudes, which motivates to completely re-think how logic synthesis for QCA circuits shall be conducted in the future.

Internet-of-Things (IoT) opens a new world of possibilities for both personal and industrial applications. At the heart of an IoT device, the processor is the core component. Hence, as an open and free instruction set architecture RISC-V is gaining huge popularity for IoT. A large ecosystem is available around RISC-V, including various RTL implementations at one end and high-speed instruction set simulators (ISSs) at the other end. These ISSs facilitate functional verification of RTL implementations as well as early SW development to some extent. However, being designed predominantly for speed, they can hardly be extended to support further system-level use cases such as design space exploration, power/timing/performance validation or analysis of complex HW/SW interactions. In this paper, we propose and implement the first RISC-V based Virtual Prototype (VP) with the goal of filling this gap. We provide a RISC-V RV321M core, a PLIC-based interrupt controller and an essential set of peripherals together with SW debug capabilities. The VP is designed as extensible and configurable platform with a generic bus system and implemented in standard-compliant SystemC and TLM-2.0. The latter point is very important, since it allows to leverage cutting-edge SystemC-based modeling techniques needed for the mentioned use cases. Our VP allows a significantly faster simulation compared to RTL, while being more accurate than existing ISSs. Finally, our RISC-V VP is fully open source to help expanding the RISC-V ecosystem and stimulating further research and development.

To close the ever widening verification gap, new powerful solutions are strictly required. One such promising approach aims in continuing verification tasks after production of a chip during its lifetime. This approach is called self-verification. However, for realizing self-verification tasks on-chip, verification packages have to be developed. In this paper, we propose verification package SAT-Lancer. SAT-Lancer is a compact Boolean Satisfiability (SAT) solver and has been implemented entirely on HW with the capability of solving any arbitrary SAT-instance. At the heart of SAT-Lancer is a scalable memory model, which can be adjusted to given memory constraints and allows to store the SAT-instance most effectively. In comparison to previous HW SAT-solvers, SAT-Lancer utilizes significant less area and can handle order of magnitude larger SAT-instances.

Nowadays, a variety of multipliers are used in different computationally intensive industrial applications. Most of these multipliers are highly parallelized and structurally complex. Therefore, the existing formal verification techniques fail to verify them. In recent years, formal multiplier verification based on Symbolic Computer Algebra (SCA) has shown superior results in comparison to all other existing proof techniques. However, for non-trivial architectures still a monomial explosion can be observed. A common understanding is that this is caused by redundant monomials also known as vanishing monomials. While several approaches have been proposed to overcome the explosion, the problem itself is still not fully understood. In this paper we present a new theory for the origin of vanishing monomials and how they can be handled to prevent the explosion during backward rewriting. We implement our new approach as the SCA-verifier PolyCleaner. The experimental results show the efficiency of our proposed method in verification of non-trivial million-gate multipliers.

Fault-free function and defect tolerance are key requirements for modern embedded systems. To meet time-to-market constraints, complex IP-components are used to assemble even more complex semiconductor products. Often, trust is required since these IPs are developed, verified and tested by external third-party IP-providers. In this work, we focus specifically on processor-IPs. A method for run-time instruction-replacement on hardware-level is presented to increase the reliability of the system. In contrast to existing techniques, our scheme can easily deal with black-box components and is comparatively lightweight. Furthermore, it includes an easy to use methodology for automated and convenient implementation. The results shows the successful application of this novel technique for reliable integration of state-of-the-art RISC-based processor-IPs.

Data flow testing (DFT) has been shown to be an effective testing strategy. DFT features a high fault detection rate while avoiding the intense scalability problems to achieve full path coverage. In this paper we propose to apply data flow testing for SystemC virtual prototypes (VPs). Our contribution is twofold: First, we develop a set of SystemC specific coverage criteria for data flow testing. This requires to consider the SystemC semantics of using non-preemptive thread scheduling with shared memory communication and event-based synchronization. Second, we explain how to automatically compute the data flow coverage result for a given VP using a combination of static and dynamic analysis techniques. The coverage result provides clear suggestions for the testing engineer to add new testcases in order to improve the coverage result. Our experimental results on real-world VPs demonstrate the applicability and efficacy of our analysis approach and the SystemC specific coverage criteria to improve the testsuite.

Efficient power management is very important for modern System-on-Chip to satisfy the conflicting demands on high performance and low power consumption. Nowadays, global power management is mostly implemented in firmware (FW) due to the relative ease of development and its flexibility. Recent advances in system-level power modeling and estimation open up opportunities for early validation of these FW-based power management strategies. In this paper, we propose a novel approach for this purpose using SystemC-based Virtual Prototypes (VPs) and constrained random (CR) techniques. The CR-generated representative system workloads are executed in a power-aware FW/VP co-simulation to validate that available performance and power budgets are satisfied. As a proof-of-concept, we demonstrate our power validation approach on the LEON3-based SoCRocket VP.

Approximate computing is an emerging methodology that allows to increase efficiency in a range of resilient applications for an affordable loss of precision or quality. In this paper, we exploit approximation in a multi-criteria optimization approach for the widely used data structure Binary Decision Diagram (BDD) to achieve higher efficiency besides lowering the inaccuracy. For this purpose, we utilize an ε-preferred evolutionary algorithm giving a higher priority to minimize BDD sizes as well as maintaining certain error constraints. In particular, we propose an adaptive ε-setting method which adds an automated factor to the algorithm based on the behavior of the function under approximation. This improves the performances of the algorithm by correcting the effect of the user set error constraints which can restrict the dimensions of the search and can lead to immature convergence.

We present ProACt, a Processor for high performance on-demand Approximate Computing. ProACt is a general purpose processor that can dynamically approximate floating point operations. In ProACt, the approximations are done in hardware, but the software can directly enable, disable or control the accuracy of approximations. In addition, ProACt offers a complete open-source development framework consisting of a hardware processor and associated software tool chain. ProACt uses functional approximations and is proven in FPGA. Further, we show performance improvements of about 30% on case studies in image processing and scientific computing.

Security is one of the most burning issues in embedded system design nowadays. The majority of strategies to secure embedded systems are being implemented in software. However, a potential hardware backdoor that allows unprivileged software access to confidential data will render even the perfectly secure software useless. As the underlying SoC cannot be patched after deployment, it is very critical to detect and correct SoC hardware security issues in the design phase. To prevent costly fixes in later stages, security validation should start as early as possible. In this paper, we propose a novel approach to SoC security validation at the system level using Virtual Prototypes (VP). At the heart of the approach is a scalable static information flow analysis that can detect potential security breaches such as data leakage and untrusted access; confidentiality and integrity issues, respectively. We demonstrate the applicability of the approach on real-world VPs.

In this paper we introduce the novel framework Yise for representing logic. Unlike the conventional approaches, Yise uses a Y-Inverter Graph (YIG) to represent the Boolean network at hand. Such a YIG represents Y-functions, which are single output, six input Boolean functions composed of three majority functions connected in a triangular (Y) fashion. We show that YIGs are a super set of the well-known and very successful logic representation data-structures AND/OR/Majority/Inverter Graphs which include AIGs and MIGs. Our results on a wide range of benchmarks show very compact representations of the logic without compromising system requirements. Up to 33% reduction in the node count can be achieved compared to AIGs without increasing the number of logic levels.

We present Approximate BDD Minimization (ABM) as a problem that has application in approximate computing. Given a BDD representation of a multi-output Boolean function, ABM asks whether there exists another function that has a smaller BDD representation but meets a threshold w.r.t. an error metric. We present operators to derive approximated functions and present algorithms to exactly compute the error metrics directly on the BDD representation. An experimental evaluation demonstrates the applicability of the proposed approaches.

Error metrics are used to evaluate the quality of an approximated circuit or to trade-off several approximated candidates in design exploration. Precisely determining the error of an approximated circuit is a hard problem since the errors accumulate over time depending on the composition and nature of individual components. In this paper, we present methods based on model checking to precisely determine error behavior in sequential circuits that contain approximated combinational components. Our experiments show that such an analysis is very significant and crucial to properly deduce the effects of approximations.

Electronic systems integrate an increasingly large number of components on a single chip. This leads to increased risk of faults, e.g. due to radiation, aging etc. Such a fault can lead to an observable error and failure of the system. Therefore, an error effect simulation is important to ensure the robustness and safety of these systems. Error effect simulation with Virtual Prototypes (VPs) is much faster than with RTL designs due to less modeling details at TLM. However, for the same reason, the simulation results with VP might be significantly less accurate compared to RTL. To improve the quality of a TLM error effect simulation, a fault correspondence analysis between both abstraction levels is required. This paper presents a case study on applying fault localization methods based on symbolic simulation to identify corresponding TLM errors for transient bit flips at RTL. First results for the interrupt controller of the SoCRocket VP, which is being used by the European Space Agency, demonstrate the applicability of our approach.

Motivated by the recent success of the algebraic computation technique in formal verification of large and optimized gate-level multipliers, this paper proposes algebraic equivalence checking for handling circuits that contain both complex arithmetic components as well as control logic. These circuits pose major challenges for existing proof techniques. The basic idea of Algebraic Combinational Equivalence Checking (ACEC) is to model the two compared circuits in form of Gröbner bases and combine them into a single algebraic model. It generates bit and word relationship candidates between the internal variables of the two circuits and tests their membership in the combined model. Since the membership testing does not scale for the described setting, we propose reverse engineering to extract arithmetic components and to abstract them to canonical representations. Further we propose arithmetic sweeping which utilizes the abstracted components to find and prove internal equivalences between both circuits. We demonstrate the applicability of ACEC for checking the equivalence of a floating point multiplier (including full IEEE-754 rounding scheme) against several optimized and diversified implementations.

Approximation circuits offer superior performance (speed and area) compared to traditional circuits at the cost of computational accuracy. The accuracy of the results in approximation circuits is evaluated based on several error metrics such as worst-case error, bit-flip error, or error-rate. Several applications have varied requirements in error metrics, i.e., all the error criteria have to be met together at a time, or in combinations. Nevertheless, all applications benefit from improved delay and area. An automated synthesis approach with formal guarantees on error metrics is very helpful in generating circuits that meet these criteria. Furthermore, each of these metrics are independent quantities (value of one metric does not correlate with the other), and automated synthesis can discover opportunities to trade off one or more of the relaxed metrics with a strict requirement on the other, resulting in better performance.

Ensuring the correctness of SystemC virtual prototypes is indispensable. For such models, existing symbolic simulation approaches are based on interpreting their behavior. In this paper we propose a major enhancement called Compiled Symbolic Simulation (CSS). For more scalable state space exploration, CSS augments the DUV to integrate the symbolic execution engine and the Partial Order Reduction based scheduler. Then, a standard C++ compiler is used to generate a native binary, whose execution performs exhaustive verification of the DUV. An extensive experimental evaluation demonstrates the potential of our approach.

Software-Driven Verification (SDV) has the promise to significantly reduce the overall time and effort for the task of IP integration and verification. With the help of SystemC Virtual Prototypes (VPs), SW tests to verify the (new) integrated IP blocks and the HW/SW integration can be developed in an early design stage and reused in the subsequent steps. However, the crucial question regarding the quality of these tests has not been considered so far. For this purpose, we propose in this paper a novel quality-driven methodology based on mutation analysis. By elevating the main concepts of mutation-based qualification to the context of SDV, our methodology is capable to detect serious quality issues in the SW tests. At its heart is a novel consistency analysis, that measures the coverage of the IP in HW/SW co-simulation in a lightweight fashion and relates this coverage to the SW test results to provide clear feedback on how to further improve the quality of tests. We provide two case studies on real-world VPs and SW tests to demonstrate the applicability and efficacy of our methodology.

To overcome the verification gap arising from significantly increased external IP integration and reuse during electronic platform design and composition, we present a model-based approach to specify platform variants. The variants specification is processed automatically by formalizing and solving the integrated constraint sets to derive valid platforms. These constraint sets enable a precise specification of the required platform variants for verification, exploration and test. Experimental results demonstrate the applicability, versatility and scalability of our novel model-based approach.

Formal verification of SystemC is challenging. Before dealing with symbolic inputs and the concurrency semantics, a front-end is required to translate the design to a formal model. The lack of such front-ends has hampered the development of efficient back-ends so far.

SystemC and Transaction Level Modeling (TLM) have become the de-facto standard for Electronic System Level (ESL) design. For the costly task of verification at ESL, simulation is the most widely used and scalable approach. Besides the Design Under Test (DUT), the TLM verification environment typically consists of stimuli generators and checkers where the latter are responsible for detecting errors. However, in case of an error, the subsequent debugging process is still very timeconsuming.

Simulation-based verification is still the state-of-the-art when checking the correctness of complex Systems-on-Chips. In particular, constraint-based simulation is popular, since here dedicated stimuli are generated which trigger certain corner-case behavior. However, to the best of our knowledge, only heuristic methods have been introduced so far. In this paper, we propose an approach that determines a minimal set of stimuli for the desired set of scenarios to be simulated. For this purpose, we are making use of solving techniques from Boolean satisfiability. Experimental evaluations demonstrate that the proposed approach can be applied to generate very compact stimuli sets. Furthermore, the proposed approach can be used to evaluate the quality of results obtained by heuristic methods.

Considerable effort is made to verify the correct functional behavior of circuits and systems. To guarantee the overall success metric-driven verification flows have been developed. In these flows coverage metrics are omnipresent. Well established coverage metrics for simulation-based verification approaches exist. This is however not the case for formal verification where property checking is a major technique to prove the correctness of the implementation. In this paper we present a guiding coverage metric for this formal verification setting. Our metric reports a single number describing how much of the circuit behavior is uniquely determined by the properties. In addition, the coverage metric guides the verification engineer to achieve completeness by providing helpful information about missing scenarios. This information comes from a new behavior classification algorithm which determines uncovered behavior classes for a signal and allows to compute the coverage of a signal. To measure the complete circuit behavior we devise a coverage metric for a set of signals. The metric is calculated by partitioning the coverage computation into a safe part and an unsafe part where the latter one is weighted accordingly using recursion. This procedure takes into account that in practice properties refer to internal signals which in turn need to be covered them-self. Overall, our metric allows to track the verification progress in property checking and significantly aid the verification engineers in completing the property set.

Simulation-based verification is still one of the most important methods to validate the correctness of System-on-Chips. Here, explicitly specified stimuli need to be generated which trigger certain scenarios of the design. However, so far stimuli generation is mainly performed independently of the desired coverage. In this work, we propose approaches for coverage-driven stimuli generation. Despite a naive method, we introduce and discuss automatic and interactive methods for an improved stimuli generation. We show that explicitly considering coverage metrics leads to smaller and complete sets of stimuli.

To meet today's time-to-market demands, catching bugs as early as possible during the design of a system is essential. In electronic system level design where SystemC has become the de-facto standard due to transaction level modeling (TLM), many approaches for verification have been developed. They determine an error trace that demonstrates the difference between the required and the actual behavior of the system. However, the subsequent debugging process is very time-consuming, in particular due to TLM-related faults caused by complex process synchronization and concurrency. In this paper, we present an automatic fault localization approach for SystemC TLM designs. We target typical TLM faults, such as accidentally swapped blocking and nonblocking transactions, erroneous event notification, or incorrect transaction data. The approach determines parts of the design that can be changed such that the intended behavior of the design is obtained by removing the contradiction given by the error trace. Single, as well as multiple faults, is considered. Techniques based on bounded model checking are used to find the faulty parts. We demonstrate the quality of our approach by several experiments. As shown in the experiments, the fault locations are identified very fast and hence a significant acceleration for the design of SystemC TLM models is achieved.

Design and verification of embedded systems at the Electronic System Level (ESL) is common practice. In particular, Transaction Level Modeling (TLM) is the major reason for the success of ESL design. However, when detailed protocols are modeled at lower levels of TLM, the verification of the communication becomes a critical issue. In this paper, we present an approach for protocol compliance checking of new or detailed protocol implementations. They are checked against user-specified protocol sequences. We also analyze the protocol coverage achieved by the testbench and visualize the results on a protocol sequence graph. Experimental results for a SoC model demonstrate the advantages of our method.

Today for System-on-Chips (SoCs) companies Electronic System Level(ESL) design is the established approach. Abstraction and standardized communication interfaces based on SystemC Transaction Level Modeling (TLM) have become the core component for ESL design. The abstract models in ESL flows are stepwise refined down to hardware. In this context verification is the major bottleneck: After each refinement step the resulting model is simulated again with the same testbench. The simulation results have to be compared to the previous results to check the functional equivalence of both models. For models at lower levels of abstraction strong approaches exist to formally prove equivalence. However, this is not possible here due to the TLM abstraction. Hence, in practice equivalence checking in ESL flows is based on simulation. Since implementing the necessary verification environment requires a huge effort, we propose an equivalence checking framework in this paper. Our framework allows to easily compare variable accesses in different SystemC models. Therefore, the two models are co-simulated using a client-server architecture. In combination with multi-threading our approach is very efficient as shown by the experiments. In addition, the time required for debugging is reduced by the framework since the respective source code references where the variable accesses did not match are presented to the user.

Electronic System Level (ESL) design manages the enormous complexity of todays systems by using abstract models. In this context Transaction Level Modeling (TLM) is state-of-the-art for describing complex communication without all the details. As ESL language, SystemC has become the de facto standard. Since the SystemC TLM models are used for early software development and as reference for hardware implementation their correct functional behavior is crucial. Admittedly, the best possible verification quality can be achieved with formal approaches. However, formal verification of TLM models is a hard task. Existing methods basically consider local properties or have extremely high run-time. In contrast, the approach proposed in this paper can verify “true” TLM properties, i.e. major TLM behavior like for instance the effect of a transaction and that the transaction is only started after a certain event can be proven. Our approach works as follows: After a fully automatic SystemC-to-C transformation, the TLM property is mapped to monitoring logic using C assertions and finite state machines. To detect a violation of the property the approach uses a BMC-based formulation over the outermost loop of the SystemC scheduler. In addition, we improve this verification method significantly by employing induction on the C model forming a complete and efficient approach. As shown by experiments state-of-the-art proof techniques allow proving important non-trivial behavior of SystemC TLM designs.

Verification is a major issue in circuit and system design. Formal methods like bounded model checking (BMC) can guarantee a high quality of the verification. There are several techniques that can check if a set of formal properties forms a complete specification of a design. But, in contrast to simulation-based methods, like random testing, formal verification requires a detailed knowledge of the design implementation. Finding the correct set of properties is a tedious and time consuming process. In this paper, two techniques are presented that provide automatic support for writing properties in a quality-driven BMC flow. The first technique can be used to analyze properties in order to remove redundant assumptions and to separate different scenarios. The second technique - inverse property checking - automatically generates valid properties for a given expected behavior. The techniques are integrated with a coverage check for BMC. Using the presented techniques, the number of iterations to obtain full coverage can be reduced, saving time and effort.

Intensive research is performed to find post-CMOS technologies. A very promising direction based on reversible logic are quantum computers. While in the domain of reversible logic synthesis, testing, and verification have been investigated, debugging of reversible circuits has not yet been considered. The goal of debugging is to determine gates of an erroneous circuit that explain the observed incorrect behavior. In this paper we propose the first approach for automatic debugging of reversible Toffoli networks. Our method uses a formulation for the debugging problem based on Boolean satisfiability. We show the differences to classical (irreversible) debugging and present theoretical results. These are used to speed-up the debugging approach as well as to improve the resulting quality. Our method is able to find and to correct single errors automatically.

In the context of formal verification Bounded Model Checking (BMC) has shown to be very powerful for large industrial designs. BMC is used to check whether a circuit satisfies a temporal property or not. Typically, such a property is formulated as an implication. In the antecedent of the property the verification engineer specifies the assumptions about the design environment and joins the respective expressions by logical AND. However, the overall conjunction may have no solution, i.e. the antecedent is contradictory. Since in this case a property trivially holds this situation has to be avoided. Furthermore, the root cause of a contradictory antecedent has to be identified which is a manual and very time-consuming process. In this paper we propose a fully automatic approach for presenting all reasons of a contradictory antecedent to the verification engineer, i.e. the approach pinpoints to the sub-expressions in the antecedent that form a contradiction. Hence, our approach reduces the debugging time of a contradictory antecedent significantly.

Synthesis of reversible logic has become a very important research area in recent years. Applications can be found in the domain of low-power design, optical computing, and quantum computing. In the past, several approaches have been introduced that synthesize reversible networks with respect to a given function. Most of these methods only approximate a minimal network representation. In this paper, exact algorithms for the synthesis of multiple-control Toffoli networks are presented, i.e., algorithms that guarantee to find a network with the minimal number of gates. Our iterative algorithms formulate the synthesis problem as a sequence of decision problems. The decision problems are encoded as Boolean satisfiability (SAT) or SAT modulo theory (SMT) instances, respectively. As soon as one of these instances becomes satisfiable, a Toffoli network representation for the given function has been found. We show that choosing the encoding for synthesis is crucial for the resulting runtimes. Furthermore, we discuss the principal limits of the SAT and SMT approaches. To overcome these limits, we propose a method using problem-specific knowledge during synthesis. In addition, better embeddings to make irreversible functions reversible are considered. For the resulting synthesis problems, an improvement is presented that reduces the overall runtime by automatically setting the constant inputs to their optimal values. Experimental results on a large set of benchmarks demonstrate the differences between three exact synthesis algorithms. In addition, a comparison with the best-known heuristic results is provided. In summary, the results show that, for some benchmarks, the heuristic approaches have already found the minimal network, while for other benchmarks, significantly smaller networks exist.

In the last years synthesis of reversible logic functions has emerged as an important research area. Other fields such as low-power design, optical computing and quantum computing benefit directly from achieved improvements. Recently, several approaches for exact synthesis of Toffoli networks have been proposed. They all use Boolean satisfiability to solve the underlying synthesis problem. In this paper a new exact synthesis approach based on Quantified Boolean Formula (QBF) satisfiability - a generalization of Boolean satisfiability - is presented. Besides the application of QBF solvers, we propose Binary Decision Diagrams to solve the quantified problem formulation. This allows to easily support different gate libraries during synthesis. In addition, all minimal networks are found in a single step and the best one with respect to quantum costs can be chosen. Experimental results confirm that the new technique is faster than the best previously known approach and leads to cheaper realizations in terms of quantum costs.

Constraint-based random simulation is state-of-the-art in verification of multi-million gate industrial designs. This method is based on stimulus generation by constraint solving. The resulting stimuli will particularly cover corner case test scenarios which are usually hard to identify manually by the verification engineer. Consequently, constraintbased random simulation will catch corner case bugs that would remain undetected otherwise. Therefore, the quality of design verification is increased significantly. However, in the process of constraint specification for a specific test scenario, the verification engineer is faced with the problem of over-constraining, i.e. the overall constraint specified for a test scenario has no solution. In this case the root cause of the contradiction has to be identified and resolved. Given the complexity of constraints used to describe test scenarios, this can be a very time-consuming process. In this paper we propose a fully automated contradiction analysis method. Our method determines all “non relevant” constraints and computes all reasons that lead to the over-constraining. Thus, we pinpoint the verification engineer to exactly the sets of constraints that have to be considered to resolve the over-constraining. Experiments have been conducted in a real-life SystemC-based verification environment at AMD Dresden Design Center. They demonstrate a significant reduction of the constraint contradiction debug time.

Formal verification is an important issue in circuit and system design. In this context, bounded model checking (BMC) is one of the most successful techniques. However, even if all the specified properties can be verified, it is difficult to determine whether they cover the complete functional behavior of a design. We propose a practical approach to analyze coverage in BMC. The approach can easily be integrated in a BMC tool with only minor changes. In our approach, a coverage property is generated for each important signal. If the considered properties do not describe the signal's entire behavior, the coverage property fails, and a counter example is generated. From the counter example, an uncovered scenario can be derived. This way, the approach also helps in design understanding. We demonstrate our method for a reduced instruction set computer (RISC) CPU. First, the coverage of the block-level verification is considered. Second, it is demonstrated how the technique can be applied on a higher level. Therefore, we investigate the instruction set verification of the RISC CPU. The experiments show that the costs for coverage analysis are comparable to the verification costs. Based on the results, we identified coverage gaps during the verification. We were able to close all of them and achieved 100% functional coverage in total.

Compact realizations of reversible logic functions are of interest in the design of quantum computers. Such reversible functions are realized as a cascade of Toffoli gates. In this paper, we present the first exact synthesis algorithm for reversible functions using generalized Toffoligates. Our iterative algorithm formulates the synthesis problem with d Toffoli gates as a sequence of Boolean Satisfiability (SAT) instances. Such an instance is satisfiable if there exists a network representation with d gates. Thus, we can guarantee minimality. In addition to fully specified reversible functions, the algorithm can be applied to incompletely specified functions. For a set of benchmarks experimental results are given.

For verification of complex system-on-chip designs often constraint-based randomization is used. This allows to simulate scenarios that may be difficult to generate manually. For the system description language SystemC the SystemC Verification (SCV) Library has been introduced. Besides advanced verification features like data introspection and transaction recording the SCV library enables constraint-based randomization forSystemC models. However, the SCV library has two disadvantages that restrict their practical use: There is no support of bit operators in SCV constraintsand the SCV constraint solver cannot guarantee a uniform distribution of the constraint solutions. In this paper we provide a detailed analysis of these problems and present solutions that have been integrated in the library.

The research in the field of reversible logic is motivated by its application in low-power design, optical computing and quantum computing. Hence synthesis of reversible logic has become a very important research area in the last years. In this paper exact algorithms for the synthesis of generalized Toffoli networks are considered. We present an improvement of an existing synthesis approach that is based on Boolean Satisfiability. Furthermore, the principle limits of the original and the improved approach are shown. Then, we propose a new method using problem specific knowledge during the synthesis process to overcome these limits. Experimental results demonstrate improvements of the overall synthesis time up to four orders of magnitude.

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

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.

Today's complex systems are modeled on a high level of abstraction. In this context, C/C++-based description languages, like SystemC, become very important. The modeling features of SystemC enable adequate levels of abstraction, hardware/software integration and fast executable specifications. Using the SystemC design methodology, a system is partitioned into hardware and software. Then the modules are refined down to the implementation. Besides efficient modeling, the correct functional behavior is very important. Already today up to 80% of the overall design costs are due to verification. As the complete system cannot be formally verified, checking of the functional behavior during operation has to be considered. In this paper an approach is presented that allows to check temporal properties for a SystemC design not only during simulation, but also after fabrication inform of an on-line test. The method translates the properties into synthesizable SystemC instructions. By this, the properties can be checked like HDL assertions during simulation and after production since they can be synthesized together with the system. The proposed approach enables a concise circuit and system verification methodology.

With ever increasing design sizes, verification becomes the bottleneck in modem design flows. Up to 80% of the overall costs are due to the verification task. Formal methods have been proposed to overcome the limitations of simulation approaches. But these techniques have mainly been applied to lower levels of abstraction. With more and more design complexity the need for hardware description languages with a high level of abstraction becomes obvious. We present a formal verification approach for circuits described in SystemC, an extension of C that allows the modeling of hardware. An algorithm for reachability analysis is proposed and a case study of a scalable bus arbiter cell is given.