Polynomial Formal Verification (PFV) ensures that a class of circuits can be verified efficiently by calculating polynomial upper bounds for the resource demands of the verification process. In this paper, we address the PFV of Boolean affine spaces represented by a 2-XOR sum of products. We show that time and space resources remain quadratic in the number of input variables during the entire verification process. Specifically, we prove that the dimensions of ROBDDs and QRBDDs representing a 2-affine space are linear. Furthermore, we prove that all ROBDDs generated during the symbolic simulation of the circuit can be computed in linear time. Finally, we provide an overall quadratic upper bound for the formal verification of QRBDD-based circuits. The experimental results confirm the given bounds.

The demand for compute-intensive applications such as AI/ML has led to the development of processors with complex functionalities. The Multiply Accumulate (MAC) unit is a vital component in these processors, but its verification is very challenging due to the highly optimized designs used to implement the MAC operation. In this paper, we show some interesting results for optimized MAC design verification using a formal proof engine, Symbolic Computer Algebra (SCA). For the first time, we exploit the combined benefit of phase and dynamic ordering in verifying MAC circuits, a capability not possible using state-of-the-art SCA proof engines.

Formally verifying divider circuits is complex, and multiple effective methods have been developed. However, none of these methods provides an upper bound on the verification time, which limits their scalability for large divider circuits. Recently, Polynomial Formal Verification (PFV) based approaches have been investigated to ensure circuit correctness in polynomial time and space. However, there is no PFV based approach for the formal verification of dividers. In this paper, we introduce for the first time a two-level partitioning strategy and present PolyRAD, a novel PFV approach for verifying Restoring Array Divider (RAD). Finally, we prove that verification of RAD can be achieved in polynomial time, and conduct experimental evaluation on RAD of different sizes to validate our theoretical findings.

Neural networks have been successfully applied in various resource-constrained edge devices, where usually central processing units (CPUs) instead of graphics processing units exist due to limited power availability. State-of-the-art research still focuses on efficiently executing enormous numbers of multiply-accumulate (MAC) operations. However, CPUs themselves are not good at executing such mathematical operations on a large scale, since they are more suited to execute control flow logic, i.e., computer algorithms. To enhance the computation efficiency of neural networks on CPUs, in this paper, we propose to convert them into logic flows for execution. Specifically, neural networks are first converted into equivalent decision trees, from which decision paths with constant leaves are then selected and compressed into logic flows. Such logic flows consist of if and else structures and a reduced number of MAC operations. Experimental results demonstrate that the latency can be reduced by up to 14.9 % on a simulated RISC-V CPU without any accuracy degradation. - The code is open source at https://github.com/TUDa-HWAI/NN2Logic

The Capability Hardware Enhanced RISC Instructions (CHERI) architecture provides fine-grained memory protection for systems, but introduces additional hardware overheads that may negatively impact performance. Evaluating and optimizing such secure architectures require benchmarks that explicitly exercise their security mechanisms. Despite the abundance of benchmarks for unhardened systems, security-aware benchmarks for CHERI-based architectures remain scarce. We address this gap by proposing a framework for generating security-aware benchmarks for CHERI-based RISC-V systems, leveraging the TestRIG tool and applying CHERI-specific post-processing to ensure valid capability usage. As a demonstration use case, we apply the generated benchmarks to evaluate an In-Memory Computing (IMC)-based acceleration of the CHERI tagged memory. Our results show best-case speedups between 6% and 11%, while also identifying scenarios in which the acceleration proves no performance benefit.

The Toffoli gate is a fundamental building block for quantum arithmetic and reversible logic, yet its efficient realization remains a major challenge in both near-term and faulttolerant quantum architectures. Recent advances in dynamic quantum circuit capabilities, including mid-circuit measurement and classical feedforward, provide new opportunities for reducing the resource overhead of non-Clifford operations. In this work, we propose a set of dynamic decomposition strategies for multi-controlled Toffoli gates that exploit adaptive circuit execution and ancilla-assisted constructions. Our methods systematically reduce entangling-gate count, T-count, and T-depth compared with conventional static decompositions, while preserving fault-tolerance guarantees. Through analytical cost models and experimental evaluation, we demonstrate that relative-phase primitives and measurement-conditioned corrections enable scalable implementations with improved depth and resource efficiency.

Approximate computing improves performance and energy efficiency for error-tolerant applications such as machine learning. Prior work has proposed approximate adder libraries for memristive crossbars using IMPLY and MAGIC stateful logic, primarily focusing on area optimization or fixed crossbar mappings. However, the impact of functional approximation under fully parallel crossbar execution remains largely unexplored. This work presents a framework for generating, mapping, and evaluating approximate Ripple Carry Adders (RCAs) implemented using MAGIC logic in memristive ReRAM crossbars under fully parallel crossbar execution. We explore a large design space by generating 458,752 approximate 8-bit RCA variants. Each design is synthesized into NOR/NOT logic and mapped onto a MAGIC crossbar at the micro-operation level. The resulting implementations are evaluated in terms of latency, memristor count, and functional accuracy using Mean Squared Error (MSE) and Mean Absolute Error (MAE). Pareto-optimal designs reveal key trade-offs between latency, area, and approximation error, highlighting the potential of MAGIC-based in-memory arithmetic for low-latency and energy-efficient computing.

Resistive RAM (RRAM) has emerged as a promising technology for in-memory computing, allowing both storage and computation within the same physical substrate. Although its ability to perform analog computations, especially multiplyaccumulate (MAC) operations, has been effectively utilized in neuromorphic systems, there has been limited research on its applicability to Boolean logic synthesis. Existing approaches typically rely on graph-based representations of Boolean functions that are mapped to column-wise MAC operations on standard RRAM crossbars. However, these representations largely inherit binary fan-in constraints from conventional logic synthesis flows, resulting in limited exploitation of MAC-level parallelism and underutilization of available crossbar resources. In this work, we address this limitation by introducing the concept of multi-input OR-Inverter Graphs (m-OIGs), which allow OR nodes with fanin greater than two to better match the accumulation semantics of MAC operations. Experimental results on standard benchmark suites demonstrate that increasing OR fan-in consistently reduces both crossbar area and total evaluation cycles, leading to improved performance and more efficient use of RRAM crossbar resources, highlighting the importance of fan-in-aware logic representations.

Advancements in emerging technologies have recently increased the traction of non-von Neumann design styles. One of the most popular design styles in this domain involves using memristors to perform logic operations in memory, known as Logic-in-Memory (LiM). Memristor Aided Logic (MAGIC) is one of such LiM based design style that is widely used given its benefits in latency and energy. Several prior works have focused on the generation of logic operations, also called microoperations, for LiM based on the MAGIC design style. Recently, the generation of SPICE netlists for MAGIC design style has been achieved by the MemSPICE tool. While this represents a significant step forward, verifying the correctness of the generated netlists still depends on SPICE-level simulations. These simulations become particularly impractical for medium-to-large designs presenting a bottleneck in the validation process. To address this limitation, in this paper, we introduce veriSiM, an automated formal verification methodology for MAGIC-based LiM. More concretely, it ensures the correctness of the generated LiM SPICE netlists against the golden reference Verilog design. Our methodology involves generating clauses from the SPICE netlists and verifying them against clauses generated from the golden reference Verilog design, using the high-performance Z3 solver to perform the equivalence checking. The clause generation process from the SPICE netlists needs to be based on several conditions, which have been identified and discussed in detail. We have used several benchmarks from ISCAS’85, ISCAS’89, and ITC’99 to demonstrate the efficacy of the veri

Virtual Prototypes (VPs) are important tools in modern hardware development. At high abstractions, they are often implemented in SystemC and offer early analysis of increasingly complex designs. These complex designs often combine one or more processors, interconnects, and peripherals to perform tasks in hardware or interact with the environment. Verifying these subsystems is a well-suited task for VPs, as they allow reasoning across different abstraction levels. While modern verification techniques like symbolic execution can be seamlessly integrated into VP-based workflows, they require modifications in the SystemC kernel. Hence, existing approaches modify and replace the SystemC kernel, or ignore the opportunity of cross-level scenarios completely, and would not allow focussing on special challenges of particular subsystems like peripherals. We propose CrosSym and SEFOS, two opposing approaches for a versatile symbolic execution of peripherals. CrosSym modifies the SystemC kernel, while SEFOS instead modifies a modern symbolic execution engine. Our extensive evaluation applies our tools to various peripherals on different levels of abstractions. Both tools’ extensive sets of features are demonstrated for (1) different verification scenarios, and (2) identifying 300+ mutants. In comparison with each other, SEFOS convinces with the unmodified SystemC kernel and peripheral, while CrosSym offers slightly better runtime and memory usage. In comparison to the state-of-the-art, that is limited to Transaction Level Modelling (TLM), our tools offered comparable runtime, while enabling cross-level verification with symbolic execution.

Formal Verification (FV) is a widely used technique for verifying whether a gate-level design is functionally equivalent to its specification. However, when verification fails due to the presence of faults, Debugging and Fault Correction (DFC) becomes essential to localize bugs and correct them. Despite the success of various automatic DFC approaches, existing methods often lack theoretical guarantees on the computational resources required, making them unpredictable in terms of time and space complexity. Therefore, it is essential to establish upper bounds on the time and space complexity of the DFC process to ensure its practical feasibility. In this paper, we rely on the CutWidth (CW) property to introduce Polynomial Debugging and Fault Correction (PDFC) as a subclass of DFC for combinational circuits, where the time and space complexities of DFC are characterized by CW. Specifically, we show that for circuits with bounded CW, the entire DFC process can be polynomially bounded, unlike Yosys SAT, which has exponential complexity. Moreover, we prove that for circuits with constant CW, the entire DFC process can be carried out in linear time and space. Finally, we evaluate several architectures of adders with small constant cutwidth, considering various numbers and locations of faulty gates in terms of time and space required for the DFC process to confirm our theoretical findings and also compare it with Yosys SAT. To demonstrate that our PDFC approach is not limited to adders and can be applied to any design with bounded cutwidth, we also evaluate benchmark circuits fromITC’99andIWLS’93in terms of time and space of the DFC process.

The hardware complexity related to the number of transistors in electronic devices used by today’s society has grown considerably in the last decades because of technological progress. In order to guarantee the correct behavior of such devices and meet time-to-market constraints, there is a need to continuously develop more efficient data structures and algorithms in formal verification. The performance of verification algorithms depends in particular on the compactness of data structures. A reduced ordered binary decision diagram (BDD) is basically a suitable data structure to verify digital circuits, as it represents Boolean functions canonically respecting a variable ordering and allows direct manipulation of them. However, one of the main challenges with BDDs is to find a variable ordering so that the BDD size of a function is compact and does not become impractical due to a dramatically increasing number of BDD nodes. To address the aforementioned issue, this article presents a novel evolution strategy having an efficient evaluation of variable ordering in a divide-and-conquer manner for BDD optimization. Experiments on benchmarks of multilevel circuits show that using this strategy results in considerably smaller BDDs being found significantly faster compared to state-of-the-art optimization techniques.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored, as they provide guaranteed polynomial upper bounds on the time and space required for the verification process. Recently, it was shown that circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP) . However, these results are limited to combinational circuits, whereas most designs used in digital systems are sequential. In this article, we introduce Linear Formal Verification (LFV) as a subclass of PFV for sequential circuits with constant cutwidth, which are verifiable in linear time and space using ASP. We achieve this by proposing a new data structure called Weighted And-Inverter Graph (W-AIG) . Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in linear time and space. Finally, we implement our approach and experimentally show that a variety of sequential circuits, such as pipelined adders, serial adders, and shift registers, can be verified in linear time and space, while ring counters can be verified in polynomial time and space, confirming our theoretical findings.

In the field of Electronic Design Automation (EDA), managing circuit complexity is a crucial task for efficient circuit verification, testing, and optimization. Increasing design complexity presents challenges for tasks such as formal verification, fault detection, and circuit optimization. Therefore, reducing circuit complexity becomes crucial in improving the efficiency and scalability of these tasks. These circuits are typically represented as graphs. In the field of parameterized complexity, CutWidth (CW) and TreeWidth (TW) are well-studied decomposition techniques that have been used in analyzing graph algorithms. In this paper, we introduce the TW decomposition technique to the field of EDA for the first time and demonstrate its impact on reducing the circuit complexity of circuits. Additionally, we present a new decomposition technique that combines both decompositions, resulting in a further reduction in circuit complexity. Furthermore, we present experimental results comparing complexity upper bounds from various decompositions to highlight the efficacy of our approach on the ISCAS’85 and EPFL benchmark circuits. Our results show that our decomposition technique outperforms the complexity upper bounds of CW by 90.16× and the complexity upper bounds of TW by 9.34× for the ISCAS’85 benchmarks. Additionally, it outperforms the complexity upper bounds of CW by 1986.37× and the complexity upper bounds of TW by 94.13× for the EPFL benchmarks. Finally, to demonstrate the applicability of the decomposition techniques in solving various EDA problems, we propose a new Formal Verification (FV) approach that leverages these techniques to provide an upper bound for the verification process. We also conduct an experimental evaluation on the ITC’99 , MCNC’91 , and VHDL Library of Arithmetic Units ( ELAU ) benchmark circuits, adder circuits of various sizes (up to 3072-bit width), and Genmul multipliers of different sizes (up to 10×10), to demonstrate the scalability of our approach.

The hardware complexity in electronic devices used by today's society has increased significantly in recent decades due to technological progress. In order to cope with this complexity, data structures and algorithms in electronic design automation must be continuously improved. Decision Diagrams (DDs) are an important data structure in the design and analysis of circuits because they allow efficient algorithms for their manipulation. The practical relevance of DDs leads to an ongoing quest for appropriate software solutions that enable working with different DD types. Unfortunately, existing DD software libraries focus either on efficiency or usability. Consequences are a disproportionately high effort for extensions or considerable loss of performance. To tackle these issues, a modular and efficient Framework to Engineer Decision Diagrams Yourself (FrEDDY) is proposed in this paper. Various experiments demonstrate that no compromise with regard to performance has to be made when using FrEDDY. It is on par with or clearly more efficient than established DD libraries.

Ensuring the functional correctness of a digital system is achievable through formal verification. Despite the increased complexity of modern systems, formal verification still needs to be done in a reasonable time. Hence, Polynomial Formal Verification (PFV) techniques are being explored as they provide a guaranteed upper bound on the run time for verification. Recently, it was shown that combinational circuits characterized by a constant cutwidth can be verified in linear time using Answer Set Programming (ASP). However, most of the designs used in digital systems are sequential. Hence, in this paper, we propose a linear time formal verification approach using ASP for sequential circuits with constant cutwidth. We achieve this by proposing a new data structure called Weighted-And Inverter Graph (W-AIG). Unlike existing formal verification methods, we prove that our approach can verify any sequential circuit with a constant cutwidth in a linear time. Finally, we also implement our approach and experimentally show the results on a variety of sequential circuits like pipelined adders, serial adders, and shift registers to confirm our theoretical findings.

Functional simulation is an essential step in digital hardware design. Recently, there has been a growing interest in leveraging Large Language Models (LLMs) for hardware testbench generation tasks. However, the inherent instability associated with LLMs often leads to functional errors in the generated testbenches. Previous methods do not incorporate automatic functional correction mechanisms without human intervention and still suffer from low success rates, especially for sequential tasks. To address this issue, we propose CorrectBench, an automatic testbench generation framework with functional self-validation and self-correction. Utilizing only the RTL specification in natural language, the proposed approach can validate the correctness of the generated testbenches with a success rate of 88.85 %. Furthermore, the proposed LLM-based corrector employs bug information obtained during the self-validation process to perform functional self-correction on the generated testbenches. The comparative analysis demonstrates that our method achieves a pass ratio of 70.13 % across all evaluated tasks, compared with the previous LLM-based testbench generation framework's 52.18% and a direct LLM-based generation method's 33.33%. Specifically in sequential circuits, our work's performance is 62.18 % higher than previous work in sequential tasks and almost 5 times the pass ratio of the direct method. The codes and experimental results are open-sourced at the link: https://github.com/AutoBench/CorrectBench.

Symbolic execution is an SMT-based software verification and testing technique. Symbolic execution requires tracking performed computations during software simulation to reason about branches in the software under test. The prevailing approach on symbolic execution of binary code tracks computations by transforming the code to be tested to an architecture-independent intermediate representation (IR) and then symbolically executes this IR. However, the resulting IR must be semantically equivalent to the binary code, making this process complex and error-prone. The semantics of the binary code are specified by the targeted instruction set architecture (ISA), commonly given in natural language and requiring a manual implementation of the transformation to an IR. In recent years, the use of formal languages to describe ISA semantics in a machine-readable way has gained increased popularity. We investigate the utilization of such formal semantics for symbolic execution of binary code, achieving an accurate representation of instruction semantics. We present a prototype for the RISC-V ISA and conduct a case study to demonstrate that it can be easily extended to additional instructions. Furthermore, we perform an experimental comparison with prior work which resulted in the discovery of five previously unknown bugs in the ISA implementation of the popular IR-based symbolic executor angr.

The popularity of compute intensive applications, like AI/ML, has driven the design of processors with complex functionality. The Dot Product (DP) is one of the most essential operations in modern neural processors, although no complete formal verification technique exists that can ensure its 100% correctness. In this paper we show the first step towards formally verifying DP using Symbolic Computer Algebra (SCA). The verification process is performed without the need of a reference model generation which is a key factor in verification. Experimental results show the efficiency and scalability of SCA-based verification for DP architectures.

In this paper, we propose a novel method for locating and diagnosing bugs in quantum circuits. Debugging in the quantum domain is especially challenging due to the inherent inability of assessing the quantum state of a program. Moreover, explaining the root cause behind unexpected outcomes is hard due to the limited information gain provided by measurements. Our approach aims to address both of these issue: Firstly, the bug site is identified using a standard circuit slicing technique combined with an associated measurement strategy. Secondly, we provide information about the nature of the bug, generated through repeated measurements. To minimize the number of measurements, we introduce a notion of equivalence classes based on unitary operations. This allows us to partition the gate library into classes that produce indistinguishable results under certain measurements. Finally, We assess the effectiveness and measurement complexity of our method by applying it to relevant primitive gate components and well-known quantum algorithms. Our empirical results shows that in 95.79% of all cases, our approach reveals the correct location of the bug along with a valid set of fault candidates. Furthermore, we demonstrate that the required number of circuit executions scales logarithmically with the circuit depth or linearly with the number of qubits.

Modern hardware design is challenged by the ever-increasing complexity of designs. An important step is hardware verification, where Virtual Prototypes (VPs) can be used for a cross-level verification throughout the refinements. Peripherals are relevant targets, because they characteristically implement a wide range of integral tasks. Symbolic execution is a popular verification method, but has been applied to SystemC peripherals only once, and never for a cross-level verification. We propose CrosSym, the first method to verify peripherals at both Register Transfer Level (RTL) and Transaction Level Modelling (TLM) abstraction with symbolic execution, explicitly supporting cross-level. Our extensive evaluation explores (1) the performance costs of two abstraction levels, (2) our approach’s suitability for a full verification, using three peripherals, (3) it’s bug finding capabilities by killing over 1500 mutants in under 15 min. In the latter, most scenarios found 97+% of the observable mutations.

In-memory Computing (IMC) using emerging devices has shown immense potential. Among these devices, memristors have emerged as one of the most popular for performing digital IMC. While several methods exist for digital IMC using memristors, most require expensive write operations in terms of energy, latency, and endurance. Hence, READ-based IMC techniques have been proposed to reduce the number of writes to the memristor crossbar. However, existing techniques rely on simple gates that can be mapped to the memristive crossbar, making them non-optimal, and they suffer from unwanted sneak paths causing undesired behavior. In this work, we alleviate these limitations and propose an optimized synthesis methodology for 1T1M crossbars called RIVER. RIVER supports more complex gates and is sneak-path aware. When comparing RIVER with the state-of-the-art using ISCAS’ 85 and EPFL benchmarks, we achieve 33% less gate utilization on average while reducing the average staircase length by 37%. Moreover, these enhancements result in a 58% reduction in the required crossbar area. After eliminating sneak paths, RIVER still shows 38% less area usage on average as compared to the state-of-the-art.

Floating-point multipliers play a crucial role in accelerating modern computing and are therefore implemented regularly, e.g., as part of AI accelerators or FPUs. They are built as a complex combination of control flow and integer arithmetic elements. This requires fast and easily applicable formal verification methods to ensure correctness. While formal verification is required to prove 100% correctness of the circuit, state-of-the-art methods fail to provide bounds for the resource and time consumption of the verification.We introduce an automated approach for formally verifying an IEEE-754-compliant floating-point multiplier with polynomial bound complexity. While state-of-the-art verification approaches based on SAT and Binary Decision Diagrams (BDDs) fail, our technique based on an adapted symbolic simulation using BDDs enables a fast and predictable verification process. Extensive case splitting is performed to prevent exponential BDD growth. The applicability is proven by verifying a single precision floating-point multiplier used in a popular floating-point unit.

Today, circuits are used in various safety-critical systems, therefore yielding a high demand for reliable systems. Consequently, a lot of research is conducted to improve the testability of designs by increasing the test coverage or reducing the required test time. In this context, provable computational bounds are crucial to ensure fast test pattern generation. Previous works proved polynomial test set generation for Binary Decision Diagram (BDD) circuits. Later, the testability of Kronecker Functional Decision Diagrams (KFDDs) was assessed, as KFDDs can exponentially reduce the required logic. However, the test set generation for KFDD circuits generally requires exponential resources. In this paper, we present a technique to derive circuits from KFDDs, for which a complete test set under the Cellular Fault Model (CFM), as well as the Stuck-At Fault Model (SAFM), can be generated within polynomial resources. The derived circuit is linear in size regarding the KFDD size, and in contrast to previously derived KFDD circuits, no redundant faults can occur, yielding fully testable circuits under CFM and SAFM. In our evaluation, the complete test set generation was up to 50 times faster than the previous exponential method, clearly showcasing the advantages of our polynomial approach.

Resistive RAM (RRAM) has emerged as a promising technology for in-memory computing by enabling storage and computation within the same physical substrate. While its analog computation capability, particularly the multiply-accumulate (MAC) operation, has been effectively used in neuromorphic systems, its potential for logic synthesis remains underexplored. Logic synthesis using MAC not only unlocks new efficiency gains but also aligns with hardware already present in neuromorphic accelerators. In this work, we present the first automated framework for evaluating arbitrary Boolean functions on standard RRAM crossbars using highly parallel MAC operations. The proposed method introduces a logic computation core for RRAM-based neuromorphic architectures without requiring additional hardware, leveraging existing peripheral circuitry. To ensure functional correctness, we further integrate a formal verification approach based on equivalence checking via SAT solvers. Experimental results on standard benchmarks demonstrate substantial reductions in computation cycles and improved efficiency compared to existing RRAM-based logic synthesis methods, highlighting the practical potential of MAC-based logic in emerging computing systems.

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

The hardware complexity in electronic devices has increased significantly in recent decades due to technological advancements. To ensure correct behavior of such devices and meet time-to-market constraints, modern circuit verification and testing tools rely on formal proof techniques. The two most popular methods in this context are Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) solvers. Even though these methods share some similarities, they are fundamentally different. Whereas BDDs usually require a large amount of memory to represent all solutions, SAT solvers are memory-efficient but they typically compute only a single solution. To tackle these issues, a hybrid approach called Binary Hybrid Diagram (BHD) is proposed for efficient generation of multiple solutions. BHDs combine the major advantages of BDDs and SAT solvers, and generate distinct solutions heuristically via algorithms. Experiments demonstrate that feasible solutions are generated rapidly by using BHDs while the memory requirement remains small compared to state-of-the-art methods.

Data-intensive Neural Network (NN) applications place high demands on data movement and computation, making the traditional von Neumann architecture inefficient. Compute-in-Memory (CIM) technology offers a promising alternative by accelerating Matrix-Vector Multiplication (MVM), the core operation in NN inference. However, the broad design space makes it challenging to identify an optimal CIM configuration. Virtual Prototypes (VPs) enable fast Design Space Exploration (DSE) across various configurations. In this work, we perform a system-level DSE by modeling a configurable CIM unit in SystemC and integrating it into a RISC-V-based VP. The CIM timing model reflects characteristics of various in-memory devices. We evaluate performance across multiple workloads, including a standalone MVM operation, a lightweight fully connected NN model, and a Convolution Neural Network (CNN) model inference. Experimental results show that the CIM unit achieves a speedup of up to 68× compared to the baseline CPU of the VP, demonstrating its effectiveness in accelerating MVM-dominated applications.

With the increasing popularity of compute intensive applications like AI, processors with complex functionalities are designed. Multiply and Accumulate (MAC) is one of the essential operations in modern Neural Processor Units (NPUs), but no sound formal verification technique exists that can efficiently ensure correctness. In this paper we analyze almost 200 configurations of MAC instances for various bit-widths starting from 8 up to several hundred bits. On top of the classical area-delay trade-off, we study verifiability as an additional parameter. It is shown that surprisingly the fastest and smallest instances are not the ones that are the hardest to verify. Exploiting Symbolic Computer Algebra (SCA) we provide a technique that allows scalable verification for large bit-width and classifies the set of MAC units.

Recent breakthroughs in Large Language Models (LLMs) and Large Circuit Models (LCMs) have sparked excitement across the electronic design automation (EDA) community, promising a revolution in circuit design and optimization. Yet, this excitement is met with significant skepticism: Are these AI models a genuine revolution in circuit design, or a temporary wave of inflated expectations? This paper serves as a foundational text for the corresponding ICCAD 2025 panel, bringing together perspectives from leading experts in academia and industry. It critically examines the practical capabilities, fundamental limitations, and future prospects of large AI models in hardware design. The paper synthesizes the core arguments surrounding reliability, scalability, and interpretability, framing the debate on whether these models can meaningfully outperform or complement traditional EDA methods. The result is an authoritative overview offering fresh insights into one of today’s most contentious and impactful technology trends.

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).

Decision Diagrams (DDs) are among the most popular representations for Boolean functions. They are widely used in the synthesis and verification of digital circuits. The size (i.e., number of nodes) and computation time (required time for performing operations) are two important parameters that determine the efficiency of a DD in different applications. It has been proven that some DDs can represent specific functions in polynomial space or perform certain operations in polynomial time. For example, Binary Decision Diagrams (BDDs) are capable of representing a wide variety of functions (e.g. integer addition) in polynomial space with respect to the input size. However, there are also some functions (e.g., integer multiplication) for which the exponential lower-bounds have been proven for the BDD sizes. In this paper, we investigate the space complexity of representing an integer addition, where one of the operands is shifted to the right by an arbitrary value. We call this function the shifted addition. This function is widely used in many digital circuits, e.g., floating point adders. We prove that the size of the BDD representing a shifted addition has exponential space complexity with respect to the input size. It is an important step towards clarifying the reasons behind the failure of BDD-based verification and synthesis when they are applied to the circuits containing shifted addition, e.g., floating point adders. • BDDs reach exponential size when symbolically simulating a floating point adder. • The lower bound for BDDs representing a shifted addition is exponential ( 2 n / 4 ). • The proof is performed by using fooling sets.

The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime in several instances. In this work, we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover’s algorithm. The Exclusive-Sum-of-Product (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover’s iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open source Qiskit platform and IBM quantum computer.

Recent studies have revealed that laser-based side-channel analysis (SCA) attack methods, particularly optical probing (OP), pose a serious threat to the security of integrated circuits (ICs). State-of-the-art countermeasures focus mainly on approaches in the domain of circuit design to mitigate the OP attack. However, methods to analyze OP, which can be integrated into the tool flow during design time, are scarce. Consequently, the actual robustness against OP can only be evaluated during post-fabrication, which may require a redesign of the IC and result in huge costs. To mitigate the lack of such methods and tools, we introduce OPTI-Sim. OPTI-Sim is an OP analysis framework, enabling designers to explore the circuit’s susceptibility against OP during design time. As OPTI-Sim allows the study of the vulnerability of the circuits against OP attacks prefabrication, it has immense potential to reduce design time and production costs of security-relevant ICs. OPTI-Sim enables an automated OP analysis at the layout level by reading layout files, performing logical computations to retrieve the state of each logic cell in the design, and performing OP analysis. The applicability of OPTI-Sim is explored by designing and evaluating a cell library and exemplary circuits that are robustified against OP attacks. Another feature of the proposed framework discussed in this work is its ability to explore the detection of hardware Trojans (HTs) using OP. HT detection using OP omits the need to have access to the golden chip to expose the HT, and results in a 100% HT detection rate. Furthermore, to the best of our knowledge, OPTI-Sim is the first OP framework of its kind.

Approximate adders have received significant attention as they give benefits in power, performance, and area for error-resilient applications. Due to their ubiquitous use, formal verification of approximate adders has also gained traction. However, prior works on formal verification of approximate adders are limited to relaxed equivalence checking, i.e., checking whether the approximate adder designs have an error less than a specified threshold. This method has limitations, as multiple approximate adder designs can satisfy the relaxed equivalence checking criterion, which can cause more than expected deterioration in the output quality. The deterioration in output quality is larger in approximate adder designs that produce exact results for some regions of the input space but have the freedom to produce approximate results in other regions of the input space. In this paper, we propose a methodology called Correct and Verify (CAV), which exploits Binary Decision Diagrams (BDDs) to guarantee that the approximate adder with correct carry bits exactly matches its functional specification. Our idea takes advantage of the BDD structure in extracting the internal signals, particularly the carry signal from the golden reference exact adder. Afterward, a corrector circuit is generated from the functional specification and the extracted carry signal is used as input in the corrector circuit. The corrector circuit is used to generate the corrected adder from the approximate adder. The generated corrected adder can be compared against a formally verified golden reference exact adder. We show the efficacy of CAV over approximate Ripple Carry Adders (RCA) as well as approximate Parallel Prefix Adders (PPA). Lastly, we perform a qualitative analysis by introducing mutations in the designs to show the fault detection quality of the CAV methodology.

Ensuring functional correctness is achieved through formal verification. As circuit complexity increases, limiting the upper bounds for time and space required for verification becomes crucial. Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In modern digital system designs, approximate circuits are widely employed in error resilient applications. Therefore, ensuring the functional correctness of these circuits becomes essential. In prior works, it has been proven that approximate circuits with constant cutwidth can be verified in linear time. However, extending binary logic verification to Multi-Valued Logic (MVL) introduces challenges, particularly regarding the encoding of MVL operators. It has been shown that MVL circuits with constant cutwidth can be verified in linear time using Answer Set Programming (ASP), due to the ASP encoding capabilities of MVL operators. In this paper, we present a PFV approach of MVL approximate circuits with constant cutwidth using ASP. We then demonstrate that the verification of MVL approximate circuits with constant cutwidth can be achieved in linear time. Finally, we evaluate various MVL approximate circuits with constant cutwidth across different logic levels to show the efficacy of our approach.

Approximate circuits have become ubiquitous in error-resilient applications. These circuits provide large reductions in area, power, and delay at the cost of erroneous computations. The error-resilient applications produce acceptable output quality, even after the introduction of erroneous computations. However, we observed that the error resilience of an application varies widely with respect to the applied inputs. Since prior works have mostly focused on using samples from a uniform distribution while designing the approximate circuits, they are unable to exploit input aware properties to design optimal circuits. Hence, in this work, we bridge this gap and propose Formally Verified Library of Input Data Aware Approximate Circuits (FV-LIDAC). FV-LIDAC is the first formally verified library of input distribution aware approximate arithmetic circuits. We use three of the most widely occurring distributions, namely uniform, normal, and exponential distributions, to show that optimal design sets are heavily dependent on the input data. FV-LIDAC chooses the best designs among millions of functional approximated adder and multiplier circuits, depending upon the inputs. Since there are no existing input-aware approximate circuit libraries, we compared FV-LIDAC against state-of-the-art input-unaware EvoApproxLib, to further highlight the need for FV-LIDAC. Additionally, we perform case studies on real-world applications to further highlight the improvement over state-of-the-art. We aim to make the Pareto-optimal designs available as open source to stimulate further research.

Continuous demands for improved performance within constrained resource budgets are driving a move from homogeneous to heterogeneous processing platforms for the implementation of today’s Real-Time (RT) embedded systems. The applications executing on such systems are typically represented as a Precedence Task Graph (PTG), where a node represents a task or algorithm for one functionality and edges represent the complex interactions between multiple functionalities. Due to RT constraints, the task graph needs to be executed within a specified deadline. Although some existing studies have looked into solving this challenge, comprehensive studies that combine the theoretical features of RT task-graph mapping and scheduling with practical runtime architectural characteristics have mostly been ignored to date. Hence, in this article, we consider the challenge of scheduling an RT application modeled as a single PTG, with the objective of minimizing the overall execution time under Hardware (HW) resource and deadline constraints for heterogeneous Central Processing Unit (CPU) + Field Programmable Gate Array (FPGA) architectures. First, we introduce an optimal solution using Integer Linear Programming (ILP). However, this ILP-based optimal solution suffers from computational complexity and does not scale well even for moderately large problem sizes. Hence, we additionally propose heuristic algorithms for task mapping and scheduling. The efficiency of the proposed scheme, named MESSI, has been evaluated through experiments using PTG on a practical CPU+FPGA system regarding current technology restrictions. Our experiments demonstrate that performance gains of 55.6% and area usage reductions of 46.3% are possible compared to full Software (SW) and HW execution, respectively.

As technology continues to advance, it becomes increasingly integrated into daily life facilitating complex tasks across a range of environments. While some applications such as smartphones and smartwatches are less critical, others like healthcare devices and autonomous vehicles demand bug-free performance to prevent financial loss or harm. Traditionally, simulation-based testing and formal verification played a major role in ensuring a bug-free device. However, the simulation of bigger systems is limited to a definite number of scenarios on the Design under Verification (DUV). Hence, it is unable to explore all possible inputs that can occur. Formal verification, on the other hand, offers a higher level of assurance through mathematical proofs but is both time-consuming and suffers from scalability issues, especially as designs grow in complexity. Recently, Large Language Models (LLMs) have shown promise in tasks previously limited to human expertise. Their natural language processing capabilities can assist in handling extensive specifications and source code, particularly in debugging hardware descriptions and analyzing security and functionality. The utilization of Retrieval Augmented Generation (RAG) has further enhanced LLMs by incorporating large specification or source code bases, thereby improving their bug-identification and correction capabilities. While recent advancements in LLMs, particularly with RAG, have yielded promising results in bug identification and correction for a small class of hardware bugs, significant gaps remain in their full potential for systematically addressing a wide range of hardware bugs. For instance, existing LLM methodologies struggle to detect bugs involving incorrect constant values, i.e., the use of wrong constants in source code. This limitation underscores the need for further exploration in utilizing LLMs to fully optimize the verification process. To bridge this gap, we propose a 3-phased 4-stage LLM-assisted systematic bug closure methodology that focuses on functional bugs in Verilog HDL rather than structural or syntactic issues. Our approach extracts functional properties of the DUV and systematically breaks down complex expressions into smaller sub-expressions to facilitate bug detection and correction. By employing RAG, the LLM is guided using the functional specifications and source code to identify and correct bugs. If the initial guidance through RAG is insufficient, our methodology initiates an iterative bug closure process. This includes incorporating more extensive information from the specifications, fetching additional lines of code for bug localization, and breaking down complex Verilog HDL expressions. In our comprehensive evaluation, we assess the LLM’s capabilities using 9 different categories of bugs. As benchmarks, we use 5 OpenTitan Intellectual Property (IP) cores to demonstrate the scalability and effectiveness of our bug closure methodology where ≈ 60% of the bugs were corrected. Specifically, we evaluate OpenAI’s GPT-4 in its ability to identify and correct functional bugs in Verilog HDL code.

In this paper, we introduce a novel set of security coverage metrics for information flow at the system level. The proposed security coverage metrics play a crucial role in assessing the qualification and quantification of various security properties, in addressing specific threat models, such as availability, and in identifying potential security vulnerabilities associated with information flow. To implement these metrics, we present SiMiT, a tool that leverages Virtual Prototypes (VP), and Static and Dynamic Information Flow Tracking (IFT) methodologies. We demonstrate the applicability of the proposed security coverage metrics through SiMiT on an open-source RISC-V VP architecture with its peripherals. By assessing the security properties using these metrics, we pave the way for a security-aware Completeness Driven Development (CDD) concept and the development of secure System-on-Chip (SoC) designs.

Existing logic-in-memory (LiM) research is limited to generating mappings and micro-operations. In this paper, we present MemSPICE, a novel framework that addresses this gap by automatically generating both the netlist and testbench needed to evaluate the LiM on a memristive crossbar. MemSPICE goes beyond conventional approaches by providing energy estimation scripts to calculate the precise energy consumption of the testbench at the SPICE level. We propose an automated framework that utilizes the mapping obtained from the SIMPLER tool to perform accurate energy estimation through SPICE simulations. To the best of our knowledge, no existing framework is capable of generating a SPICE netlist from a hardware description language. By offering a comprehensive solution for SPICE-based netlist generation, testbench creation, and accurate energy estimation, MemSPICE empowers researchers and engineers working on memristor-based LiM to enhance their understanding and optimization of energy usage in these systems. Finally, we tested the circuits from the ISCAS’85 benchmark on MemSPICE and conducted a detailed energy analysis.

Trust in electronic devices is dependent on their safe and reliable behavior. An integral part is the correct design of the hardware. While classically simulation-based approaches have been applied, only through formal proof techniques complete correctness can be guaranteed. The core of these formal approaches, and responsible for time and space complexity, is the choice of the underlying data structure to represent the functional behavior. A significant class of data structures are graph-based function representations, like BDDs, KFDDs or *BMDs. These have shown excellent properties – provability in polynomial time and space – for some function classes, e.g., adders. Experimental studies have validated these properties, and formal proofs can guarantee this behavior. Unfortunately, these properties often cannot be generalized to varying function classes. One reason is that graph-based representations are usually tailored for either bit-level or word-level functions. However, designing hybrid data structures that can represent both types in parallel might allow formal proofs for even larger functional classes.In this paper, we demonstrate how to design these hybrid data structures, overcoming limitations of current formal verification approaches. We introduce a generalized concept on decompositions and graph-based function representations based on Kronecker matrices with an extended element space and dimension. It is shown how these extensions allow the representation of hybrid function classes, paving the way for more trust in electronic devices.

Large Language Models (LLMs) have gained immense popularity and are being explored for use in several domains. In this paper, we describe the LLMs for their use in the Electronic Design Automation (EDA) domain specifically for hardware verification. LLMs are being rapidly explored for hardware design generation and verification. However, given the inherent non-determinism and the limited capabilities of the current LLMs, the designs may contain bugs or the generated properties could be incorrect. The process of manually checking these bugs can be tedious and time-consuming. This highly limits the applicability of the LLMs. Researchers are looking to alleviate these limitations by incorporating verification strategies using the LLMs and enhancing the LLMs’ capabilities not only for bug-free design generation but also stand-alone for verification. The current pace of development in these can cause many areas to be overlooked. Therefore in this work, we discuss the state-of-the-art tools and frameworks available for utilizing LLMs for EDA. We will then discuss the hardware verification techniques being explored using LLMs. We then discuss the consistency of the natural language properties generated using LLMs. Lastly, we will discuss the future directions in which the LLMs can aid in the hardware verification process.

Resistive RAM (RRAM) is a non-volatile memory technology with an abrupt switching property that enables it to perform basic logic operations. RRAM also possesses analog computational features by means of the so-called Multiply and Accumulate (MAC) operation that can be performed in all memory columns simultaneously. The MAC operation is particularly interesting for neuromorphic computing as it enables highly parallelized calculation of complex matrix-vector multiplications on standard RRAM crossbars.So far, several forms of universal logic are executed within RRAM devices, which have been the basis for a variety of logic-in-memory synthesis approaches. Recent research has addressed the mapping of logical functions to RRAM crossbars using the MAC operation, which allows for the facilitation of RRAM-based neuromorphic architectures with a basic logical core. Recently, a few formal verification methods have been introduced, which are tailored for synthesis approaches using certain RRAM logic primitives, such as in-memory styles based on the three-input majority operation and NOR gates. This paper analyzes these methods and, for the first time, proposes a verification method customized for MAC-based in-memory computing. A case study has been conducted to compare the proposed method with the existing methods, which reveals the superior performance of our method.

The ability of resistive memory (ReRAM) to naturally conduct vector-matrix multiplication (VMM), the primary operation carried out in neural networks, has caught the interest of researchers. The memristor crossbar is a suitable architecture to perform VMM and additionally offers benefits like in-memory computation (IMC), low power, and high density. Memristor-based neural networks are typically trained using a mechanism where weight computations are carried out on a host machine and downloaded into the crossbar. However, due to faulty memristors in the crossbar, a cell may not be able to store the exact weight values, which may lead to inference errors. In this paper, we propose a weight-sharing method to improve the self-fault-tolerance capability of memristor crossbar. In order to reduce the impact of faulty memristors, the weights are shared among different layers of memristors in a 3D crossbar. Simulation analyses show considerable improvements in the fault-tolerance capability of the crossbar.

Magnetic Resonance Imaging (MRI) is an essential tool for medical diagnosis. At the same time, its usage requires profound expert knowledge to determine the ideal MR sequence and protocol to be run. Until now, the contrast and quality of the resulting image have relied mainly on the radiologist's expertise. When confronted with clinical requirements and patient information, the radiologist chooses suitable sequence protocols for the examination. We propose a workflow that supports medical personnel in finding the optimal sequence for a given diagnostic task. To that end, we combine evolutionary algorithms for the optimisation, machine learning techniques for training a surrogate optimisation function from simulated MRI data, and domain-specific languages to allow non-programmers to formulate their requirements and constraints semi-formally. In this paper, we focus on the efficient usage of real-world application-motivated adaptions of the used evolutionary algorithm and evaluate their effects on four real-life sequence examples. We show that it is essential to use an adaption for the surrogate model to obtain realistic solutions and use correlation information about the search space to stay in feasible areas of the search space and thus improve optimisation quality. These findings are a first step in automating the entire MRI-sequence optimisation flow, which is necessary to allow a more widespread usage of this essential medical diagnostic technique.

In this paper, we present an optimized methodology for performing state-space-based equivalence checking of nonlinear analog circuits by using a gradient-ascent-based search algorithm to efficiently traverse a common state space. Essentially, the method searches for critical regions where the functional behaviors of two circuit designs show the greatest divergence. The key challenges in this approach are the mapping of both designs onto a common canonical state space, the computation of the gradient, and the exclusion of unreachable regions within the state space. To address the first challenge, we use locally linearized systems and leverage the Kronecker Canonical Form (KCF). To facilitate the computation of the gradient, we employ a purpose-built target function, and to exclude unreachable regions, we utilize vector projection techniques. Through experiments with nonlinear analog circuits and a scalability analysis, we demonstrate the successful and efficient computation performed with the proposed methodology, achieving speedups of up to 468 times.

In this paper, we propose a methodology for hardware verification assisted by Large Language Models (LLMs) in the incremental proof generation process. First, an LLM identifies the basic module of the Design Under Verification (DUV), followed by expanding the proof scope as more modules are added. LLMs assist in defining and verifying invariants for each module using the Z3 solver, and in formulating integration properties at module interfaces. Our case studies on a Ripple Carry Adder (RCA) and a Dadda Tree Multiplier (DTM) demonstrate that LLMs enhance the efficiency and accuracy of hardware verification.

The increasing complexity of modern hardware designs poses significant challenges for design verification, particularly defining and verifying properties and invariants manually. Recently, Large Language Models (LLMs) such has GPT-4 have been explored to generate these properties. However, assessing the quality of these LLM generated properties is still lacking. In this paper, we introduce a LLM-guided formal verification methodology combined with mutation testing for creating and assessing invariants for Design Under Verification (DUV). Utilizing OpenAI's GPT-4, we automate the generation of invariants and formal models from design specifications and Verilog behavioral models, respectively. We further enhance this approach with mutation testing to validate the quality of the invariants. We use a 27-channel interrupt controller (C432) from ISCAS-85 benchmarks as a complex case-study to showcase the methodology.

Recently, the concept of Polynomial Formal Verification (PFV) has been introduced and successfully applied to several classes of functions, allowing complete verification under resource constraints. But so far, all studies were carried out for combinational circuits only. In this paper we show how the concept of PFV can be extended to sequential circuits. As a first case study we show for counters that PFV can be performed, even though they have an exponential number of states, i.e., they can be fully formally verified within polynomial upper bounds on run-time and memory requirement.

Dynamic Quantum Circuits (DQC) is an inevitable solution for today's Noisy Intermediate Scale Quantum (NISQ) systems. This enables realization of an n-qubit (where,$n > 2$) quantum circuit using only 2-qubits with the aid of additional non-unitary operations which is evident from the recent dynamic realizations of algorithms like Quantum Phase Estimation (QPE) and Bernstein- Vazirani (BV) as well as 3-qubit Toffoli operation. In this work, we introduce two different dynamic realization schemes for Multiple Control Toffoli (MCT) gates, for the first time to the best of our knowledge. We compare the respective realizations in terms of resources (e.g., gate, depth and nearest neighbor overhead) and computational accuracy. For this purpose, we apply the proposed dynamic MCT gates in Deutsch-Jozsa (DJ) algorithm, thereby realizing the traditional DJ algorithm as DQCs. Experimental evaluations show that one dynamic scheme for MCT gates leads to DQCs with better computational accuracy, while the other one results in DQCs with better computational resources.

Reconfigurable Field Effect Transistors (RFETs) can be programmed on the fly to behave either as NMOS or PMOS. Digital circuit designs using RFETs have been shown to benefit both in design and security metrics compared to traditional FETs. In this paper, we highlight the problem associated with the cascading of RFET-based logic cells that have their Source(S)/Drain(D) terminals not connected to the supply Voltage(VDD)/Ground(GND). While these circuits occupy a lesser area, there is a drastic increase in the delay of these logic cells when they are cascaded as a result of the S/D being driven by inputs. We then discuss two methods to mitigate this issue using a) buffer insertion for delay minimization, and b) logic cells that have their S/D terminals driven by VDD/GND.

Formal verification techniques are computationally complex and the exact time and space complexities are in general not known, which makes the performance of the process unpredictable. Some of the recent works have shown that it is possible to carry out formal verification with polynomial time and space complexities for specific designs like arithmetic circuits. However, the methodology used cannot be directly extended to complex designs like processors. A recent work has shown polynomial verification of a single-cycle RISC- V processor with limited functionality, which considers only the combinational parts of the AL U. In this paper we propose for the first time a complete verification approach that covers all the functional units of the processor, and at the same time considers its sequential behavior. Experimental results show that the verification can be carried out in polynomial time, and also demonstrate significant improvement over previous methods.

Tailoring hardware to an application significantly enhances its performance compared to using a general-purpose processor. While hardware optimization is essential to meet the user requirements for resource-constrained embedded systems, it generally entails considerable costs and a high level of effort. In recent work virtual prototypes have been shown to be an effective analysis tool for guiding this process. In best-case scenarios, it is possible to identify a single recurring instruction sequence that covers approximately 55 % of all executed instructions and is thus suitable for optimization by a Hardware Accelerator (HA). However, challenges arise for applications where each identified sequence only covers a small fraction of the total execution. In order to achieve comparable coverage, several HAs can be designed, but this also multiplies the hardware costs. To address these issues, this work proposes an approach to extend and merge identified sequences allowing the design of a single HA for the merged sequence. Experiments show that this approach significantly increases the coverage achievable with a single HA while the resulting performance loss is negligible compared to building multiple HAs.

As hardware designs are getting more complex, verification becomes ever more important to prevent producing chips which do not behave according to their specification. This increasing complexity also impacts the verification process, resulting in a longer time-to-market. Ensuring that the verification itself can be conducted efficiently helps facing these challenges. Additionally, taking the efficient verification into consideration during the design phase further enables the optimization of the whole process. In this paper, we present a SAT-based verification flow and how it can ensure polynomial bounds for the verification of circuits with limited cutwidth. To demonstrate our approach, the flow is applied to three different adder architectures. Addition is one of the most essential operations in digital computations and the simplicity of its circuit realizations makes it a good starting point to explore their efficient verification using SAT. We provide theoretical proofs that SAT can be used for Polynomial Formal Verification (PFV) of circuits with limited cutwidth. We then show that for the considered adder circuits, a linear time complexity of the verification process can be ensured and confirm our findings by experimental evaluation with our own SAT solver.

IEEE Std. 1687 (IJTAG) introduces reconfigurable scan networks that implement an effective test access in highly complex designs. Designing an optimized network, that provides access to the instruments, meets the non-functional constraints, and preserves a minimized routing effort, area overhead and test access time, forms a non-trivial optimization problem. This paper tackles the IJTAG network topology design challenge by proposing an evolutionary approach to synthesize reconfigurable scan networks with optimized routing and area overhead while minimizing the overall test time.

In the context of digital circuits, formal verification methods have been well-studied to ensure their functional correctness. However, several verification methods fail to provide an upper bound for the time and space complexity. Therefore, Polynomial Formal Verification (PFV) has been introduced to address this problem. Unlike prior works, which have shown that approximate circuits can be verified in polynomial time, we show that approximate circuits with a constant cutwidth can be verified even in linear time. Since approximate circuits have become ubiquitous in error-resilient applications, it becomes essential to guarantee their correctness. While prior works have been limited to formal error analysis, we use Answer Set Programming (ASP) based formal verification to guarantee that the approximate circuit matches its functional specification. In this paper, we first show that several approximate adder circuits exhibit a constant cutwidth. We then provide a PFV approach that relies on this cutwidth as a structural property of the circuits to guarantee a linear-time verification w.r.t. the bitwidth using ASP. Finally, we evaluate several approximate adders in terms of the upper bound of the cutwidth, and verification time.

In this paper we present the first Decision Diagrams (DDs) based methodology for verifying the Resistive Random Access Memory (ReRAM) synthesis process. In particular, we propose a methodology which leverages Binary Decision Diagrams (BDDs), Multiplicative Binary Moment Diagrams (*BMDs), and Kronecker Multiplicative BMDs (K*BMDs) for verification. We introduce a synthesis tool for ReRAM-compatible micro-operations and a DD generation process for equivalence checking. Experimental results on a large set of arithmetic adders demonstrate that our DD-based approach significantly outperforms SAT solvers in verification speed, offering a more efficient and scalable solution.

In-memory computing (IMC) has gained signifi- cant attention recently as it attempts to reduce the impact of memory bottlenecks. Numerous schemes for digital IMC are presented in the literature, focusing on logic operations. Often, an application's description has data dependencies that must be resolved. Contemporary IMC architectures perform read followed by write operations for this purpose, which results in performance and energy penalties. To solve this fundamental problem, this paper presents in-memory mirroring (IMM). IMM eliminates the need for read and write-back steps, thus avoiding energy and performance penalties. Instead, we perform data movement within memory, involving row-wise and column-wise data transfers. Additionally, the IMM scheme enables parallel cloning of entire row (word) with a complexity of O(1). Moreover, we analyzed the energy consumption of the proposed technique on an RRAM crossbar with an experimentally validated JART VCM v1b model. The IMM increases energy efficiency and shows 2x performance improvement compared to conventional data movement methods.

In this work mapping of quantum circuits to regular hexagonal grid with coupling degree of six has been investigated. Architectures involving superconducting qubits impose restrictions on 2-qubit gate operations to be carried out only between physically coupled qubits, also referred to as nearest-neighbor (NN) constraint. The noise introduced by the 2-qubit gates and the execution time greatly affect the computational reliability. Existing mapping techniques suffer either from the adopted approach to reduce gate overhead or from their inability to take advantage of such architectural regularity. We outlined three different qubit mapping approaches using Remote-CNOT templates, Swap gates and combination of both. We show the benefits of assigning the Cartesian coordinate system in hexagonal grid for runtime elevation and devised approaches for reduction in gate overheads. While the template-based approach gives a strict upper bound of additional gate overheads for a particular qubit mapping, the combined approach provides better result employing a larger lookahead window. Experiments on benchmark quantum circuits confirm that the proposed Swap-based method provides an average \(25\%\) improvement in gate overheads over a recent work and the combined approach contributes further \(15\%\) average improvement on the result at the expense of a little higher runtime.

The success of idea crowdsourcing platforms relies on fostering a collaborative environment that encourages active user participation, measured by the quality and quantity of contributions and interactions. However, understanding the impact of peer interactions on user engagement and the innovation process remains challenging. While previous studies have focused on sentiment analysis, the contextual interpretation of peer feedback and its effects on engagement and innovation have yet to be explored. To address this knowledge gap, we propose a feature-based AI model that categorizes peer feedback based on its quality and polarity. Our model achieves 96% accuracy in identifying feedback quality (constructive vs. non-constructive and toxic vs. non-toxic) and feedback polarity (negative vs. positive). This contextual feedback categorization provides a foundation for quantitatively analyzing the impacts of feedback on user engagement and the innovation process. Our results show that positive and constructive peer feedback has a significantly positive effect, while toxic and negative peer feedback has a significantly negative impact on the process of idea generation, idea evaluation, and idea selection. Our results also indicate that inexperienced users are more susceptible to toxic feedback than experienced users. Based on these findings, we suggest a recommendation and reward system for incentivizing constructive feedback and preventing toxic feedback.

Approximate circuits have become ubiquitous in error-resilient applications. Given their widespread use, formal verification of these approximate designs is essential. Recently, there have been attempts that use formal verification techniques based on Boolean Satisfiability (SAT) Methods and Binary Decisions Diagrams (BDDs) to perform formal error analysis. These methods guarantee that the designed approximate circuits satisfy the error metrics, e.g., Mean Square Error (MSE), etc. However, in certain approximate circuits tailored for a particular input data distribution, only performing error analysis is not enough. In addition to error metrics, the functional specifications in these approximate circuits should also be satisfied. Otherwise, it can lead to a larger-than-expected deterioration in the output quality. In this work, for the first time, we alleviate this issue by proposing an automated formal verification methodology, cecApprox, that guarantees the approximate circuit matches the functional specification. This is crucial for circuits that are tailored for a particular input distribution. We show that in the designs where the structure is preserved, the corrected circuit can be generated from the approximate circuit. This corrected circuit can then be formally verified by performing combinational equivalence checking with the exact circuit as the golden reference. If the corrected circuit is equivalent to the exact circuit, it guarantees that the approximate circuit matches the given functional specification in addition to error metrics. Hence, the cecApprox methodology complements the formal error analysis method. We show the efficacy of cecApprox by generating and formally verifying millions of different 8-bit and 16-bit structural preserved approximate adders and multipliers using combinational equivalence checking.

In-Memory Computing (IMC) using memristors has gained significant interest in recent years as it addresses the issue of memory bottleneck in the von Neumann architectures. One of the most popular design styles that have been developed to perform memristor-based IMC is Memristor-Aided loGIC (MAGIC). MAGIC design style based NOR and NOT operations can be used to perform IMC on memristor crossbars. The state-of-the-art SIMPLER MAGIC tool is used to generate a mapping of any arbitrary Boolean function to MAGIC operations that are suitable for high-throughput applications. The correctness of the mapping is examined by tedious manual inspections and functional simulations which may not account for all the edge cases which is not desirable. In this work, we alleviate this issue to the best of our knowledge for the first time by proposing veriSIMPLER. veriSIMPLER is an automated formal verification methodology to ensure the functional correctness of the mapping obtained using the SIMPLER MAGIC tool. The veriSIMPLER methodology generates Boolean Satisfiability Formulas (SAT) of the mapping obtained using the SIMPLER MAGIC tool and the golden reference Verilog designs. These SAT formulas are verified against each other using the Z3 solver. The veriSIMPLER methodology identified a critical bug in the mapping obtained from the SIMPLER MAGIC tool when buffers are connected between input and output. We also propose a methodology to patch this bug to generate the correct mapping, which in turn extends the capability of the SIMPLER MAGIC tool to handle buffers on top of providing a formal verification methodology. We have used a variety of benchmark circuits from the widely used ISCAS’85, ISCAS’89, ITC’99, and IWLS’93 to show the efficacy of the veriSIMPLER methodology. We aim to make the formally verified mapping obtained using the veriSIMPLER methodology open-source to promote further research in this direction.

Recent advancements in the fabrication of Resistive Random Access Memory (ReRAM) devices have led to the development of large-scale crossbar structures. In-memory computing architectures relying on ReRAM crossbars aim to mitigate the processor-memory bottleneck that exists with current complementary metal-oxide semiconductor technology. With this motivation, several synthesis and mapping approaches focusing on the realizations of Boolean functions in the ReRAM crossbars have been proposed earlier. Thus far, the verification of the designs realized on ReRAM crossbars is done either through manual inspection or using simulation-based approaches. Since manual inspections and simulation-based approaches are limited to smaller designs, they cannot be applied to the verification of complex designs on large-scale ReRAM crossbars. Motivated by this, we propose, for the first time, an automatic equivalence checking flow that determines the equivalence between the original function specification (e.g., Majority-inverter Graph ) and the crossbar micro-operations file formats. We consider two crossbar structures, zero-transistor, one-memristor (0T1R) and one-transistor, one-memristor (1T1R) to implement the micro-operations. While the micro-operations file format exists for 0T1R crossbar structures, no representations for micro-operations to be executed in 1T1R crossbars exist yet. In this work, we introduce the micro-operation file format for 1T1R crossbar structures to efficiently represent the micro-operations as ReRAM crossbar netlists. Afterwards, we introduce two intermediate data structures, ReRAM Sequence Graph for 0T1R crossbars (ReSG-0T1R) and for 1T1R crossbars (ReSG-1T1R) , that are derived from the 0T1R and 1T1R crossbar micro-operations file formats, respectively. These ReSGs are then translated into Boolean Satisfiability (SAT) formula, and then the verification is done by checking the generated SAT formulae against the golden functional specification (represented in Verilog) using Z3 Satisfiability solver. Experimental evaluations confirm the effectiveness of the proposed verification methodology on MCNC and ISCAS benchmarks.

Virtual Prototypes (VPs) at the Electronic System Level (ESL) are being increasingly adopted by the semiconductor industry and play an important role in modernizing the System-on-Chips (SoCs) design flow to raise design productivity and reduce time-to-market constraints. Due to their early availability and significantly faster simulation speed in comparison to Register Transfer Level (RTL) designs, VPs are used as reference models for lower levels of abstraction. Leveraging VPs and extending their use cases for early security validation are shown as a promising direction. As the cost of fixing any security flaws increases with the stage of development, VP-based security validation can significantly avoid costly iterations. In this article, we present a novel VP-based dynamic information flow analysis approach at the ESL, consisting of three main phases which are runtime behavior extraction (in terms of transactions), transactions transformation, and security validation. The proposed approach empowers designers to validate the information flow policies of a given VP-based SoC against the most occurring security threat models which are information leakage (confidentiality) and unauthorized access to data in a memory (integrity). Experimental results including an extensive set of standard benchmarks and two real-world VP-based SoCs demonstrate the scalability and applicability of the proposed approach.

Recent progress in the fabrication of Resistive Random Access Memory (ReRAM) devices has paved the way for large scale crossbar structures. In particular, in-memory computing on ReRAM crossbars helps in bridging the processor-memory speed gap for current CMOS technology. To this end, synthesis and mapping of Boolean functions to such crossbars have been investigated by researchers. However the verification of simple designs on crossbar is still done through manual inspection or sometimes complemented by simulation based techniques. Clearly this is an important problem as real world designs are complex and have higher number of inputs. As a result manual inspection and simulation based methods for these designs are not practical.

In recent years, hardware systems have significantly grown in complexity. Due to the increasing complexity, there is a need to continuously improve the quality of the hardware design process. This leads designers to strive for more efficient data structures and algorithms operating on them to guarantee the correct behavior of such systems through verification techniques like model checking and meet time-to-market constraints. A Binary Decision Diagram (BDD) is a suitable data structure as it provides a canonical compact representation of Boolean functions, given variable ordering, and efficient algorithms for manipulating them. However, reduced ordered BDDs also have challenges: There is a large memory consumption for the BDD construction of some complex practical functions and the use of realizations in the form of BDD packages strongly depends on the application.

With the exponential increase in the popularity of the RISC-V ecosystem, the security of this platform must be re-evaluated especially for mission-critical and IoT devices. Besides, the insertion of a Hardware Trojan (HT) into a chip after the in-house mask design is outsourced to a chip manufacturer abroad for fabrication is a significant source of concern. Though abundant HT detection methods have been investigated based on side-channel analysis, physical measurements, and functional testing to overcome this problem, there exists stealthy HTs that can hide from detection. This is due to the small overhead of such HTs compared to the whole circuit.

Adapting optimisation algorithms, such as evolutionary algorithms, to a problem is a necessity. The required collection and exchange of domain information is an important but tedious task in real-world projects involving several experts from different areas of expertise (e.g. the domain and the optimisation area). This paper presents a structured approach that allows the experts to systematically provide their knowledge using domain-specific languages. The presented approach defines a different language for the involved experts that enables them to add their knowledge and use the information provided by other experts. The languages are extensible, allowing the addition of new optimisation aspects without changing the actual language. These languages are the front-end to a versatile open-source optimisation tool, that we built, enabling the actual execution of the optimisation. It additionally provides features for surrogate models as well as data generation and different benchmarks for evaluation. Conducting a user study, we show that the language is suitable to express the domain knowledge and domain experts can use the language to describe their domain knowledge after a short introduction. This way, the approach reduces the effort for domain experts in providing their information. As a side effect, the complete configuration of the optimisation execution through these languages allows an easy and reliable reproduction.

We propose to leverage state-of-the-art symbolic execution techniques from the Software (SW) domain for processor verification at the Register-Transfer Level (RTL). In particular, we utilize an Instruction Set Simulator (ISS) as a reference model and integrate it with the RTL processor under test in a co-simulation setting. We then leverage the symbolic execution engine KLEE to perform a symbolic exploration that searches for functional mismatches between the ISS and RTL processor. To ensure a comprehensive verification process, symbolic values are used to represent the instructions and also to initialize the register values of the ISS and processor. As a case study, we present results on the verification of the open source RISC-V based MicroRV32 processor, using the ISS of the open source RISC-V VP as a reference model. Our results demonstrate that modern symbolic execution techniques are applicable to a full scale processor cosimulation in the embedded domain and are very effective in finding bugs in the RTL core.

Recently, Signal Flow Graphs (SFGs) have been successfully leveraged to show equivalence for linear analog circuits at system-level and SPICE-level. However, this is clearly not sufficient as the true complexity stems from nonlinear analog circuits. In this paper, we go beyond linear analog circuits, i.e., we extend the SFGs and develop the Modified Signal-Flow Graph (MSFG), to show equivalence between system-level and SPICE-level representations of static nonlinear analog circuits. First, we map the nonlinear circuits to MSFGs. Afterwards, graph simplification and functional approximation (in particular Legendre polynomials) techniques are used to create minimal MSFG and canonical MSFG. This enables us to compare the MSFGs even if they have vastly different structures. Finally, we propose a similarity metric that calculates the similarity between SPICE-level and system-level models. By successfully applying the proposed equivalence checking technique to benchmark circuits, we demonstrate its applicability.

With the rapid growth in the size and complexity of digital circuits, the possibility of bug occurrence has significantly increased. In order to avoid the enormous financial loss due to the production of buggy circuits, using scalable formal verification methods is essential. The scalability of a verification method for a specific design is proven by showing that the method has polynomial space and time complexities. Unfortunately, not all verification methods have a polynomial complexity, particularly when it comes to the verification of large and complex designs. In this paper, we propose a divide-and-conquer strategy for Polynomial Formal Verification (PFV) of complex circuits. Instead of using a monolithic proof engine to verify the entire design, we break the verification task down into several problems, which can be solved in polynomial space and time using a hybrid proof engine. As a case study, we investigate the PFV of the ALU in a RISC-V processor using our divide-and-conquer strategy.

In this paper, we present our verifier that takes advantage of Binary Decision Diagrams (BDDs) with case splitting to fully verify a floating point adder. We demonstrate that the traditional symbolic simulation using BDDs has an exponential time complexity and fails for large floating point adders. However, polynomial bounds can be ensured if our case splitting technique is applied in the specific points of the circuit. The efficiency of our verifier is demonstrated by experiments on an extensive set of floating point adders with different exponent and significand sizes.

Recent advances in fault tolerant quantum systems allow to perform non-unitary operations like mid-circuit measurement, active reset and classically controlled gate operations in addition to the existing unitary gate operations. Real quantum devices that support these non-unitary operations enable us to execute a new class of quantum circuits, known as Dynamic Quantum Circuits (DQC). This helps to enhance the scalability, thereby allowing execution of quantum circuits comprising of many qubits by using at least two qubits. Recently DQC realizations of multi-qubit Quantum Phase Estimation (QPE) and Bernstein-Vazirani (BV) algorithms have been demonstrated in two separate experiments. However the dynamic transformation of complex quantum circuits consisting of Toffoli gate operations have not been explored yet. This motivates us to: (a) explore the dynamic realization of Toffoli gates by extending the design space of DQC for Toffoli networks, and (b) propose a general dynamic transformation algorithm for the first time to the best of our knowledge. More precisely, we introduce two dynamic transformation schemes (dynamic-1 and dynamic-2) for Toffoli gates, that differ with respect to the required number of classically controlled gate operations. For evaluation, we consider the Deutsch-Jozsa (DJ) algorithm composed of one or more Toffoli gates. Experimental results demonstrate that dynamic DJ circuits based on dynamic-2 Toffoli realization scheme provides better computational accuracy over the dynamic-1 scheme. Further, the proposed dynamic transformation scheme is generic and can also be applied to non-Toffoli quantum circuits, e.g. BV algorithm.

Optical Probing (OP) has been shown to be capable of retrieving intellectual property of the chips. However, to design a robust circuit against OP, the chip must be designed, fabricated, and optically probed in an experimental setup to determine the OP robustness of the design which is time consuming. To mitigate the aforementioned problems, we propose a simulation framework, namely FELOPi, which takes the layout file format of a design as an input and then performs OP on it. FELOPi can help designers to design robust circuits toward OP attacks before fabricating the chip. Hence, utilizing FELOPi results in tremendous time and cost reduction.

Reconfigurable transistors are a new emerging type of device, which offer the promise to improve the resistance of electronic components against know-how theft. In order to enable a product development of such an emerging device, a cross-layer design enablement strategy is needed, as emerging technologies are not necessarily compatible withstandard tools used in the industry. In ‘CirroStrato’, we aim on the development of such a complete flow enabling CMOS co-integration of reconfigurable transistors, ranging from process adjustments, device modeling, library characterization, physical and logical synthesis up towards sophisticated hardware security tests. In this multi-partner-project (MPP) paper, our aim is to elucidate the overall design enablement flow, as well as current research challenges on the individual stages.

The complexity of hardware systems has increased significantly in recent decades. Due to increasing user requirements, there is a need to develop more efficient data structures and algorithms to guarantee the correct behavior of such systems. A Reduced Ordered Binary Decision Diagram (BDD) is a suitable data structure as it represents all Boolean functions canonically given a variable order as well as provides algorithms for efficient manipulation. However, BDDs also have challenges: practicability depends on their minimization and there is a large memory consumption for some complex functions.To address these issues, this work investigates the number of emerged intermediate nodes that are not used in the final BDD result and presents a novel approach for efficient BDD manipulation by reducing the number of such nodes. Experiments on BDD benchmarks show that peak BDD node sizes can be significantly reduced, leading to accelerated BDD manipulation.

Nowadays, the manufacturing of Integrated Circuits (ICs) is highly distributed over different foundries yielding untrustworthy supply chains. This circumstance leads to concerns regarding the security, privacy, and reliability of the fabricated ICs, e.g., malicious usage and counterfeiting. Logic Locking (LL) is a prominent protection technique to safeguard against such concerns. Recently, the emerging technology of Reconfigurable Field-Effect Transistors (RFETs) has been utilized to implement new mechanisms based on Polymorphic Logic Gates (PLGs) to protect Intellectual Property (IP). The mechanisms’ assessment is indispensable to reinforce the newly introduced logic obfuscation and, hence, avoid any security breaches. So far, formal SAT-based and approximate Hamming Distance (HD)-based assessment techniques have been used for determining the protection quality. While the approximate and formal approaches can detect many security threats [1], they are still unable to detect optimization-based attacks. This work proposes a novel formal approach based on Pseudo Boolean Optimization (PBO) to assess the quality of LL structures for sequential circuits, enabling the detection of currently unconsidered security breaches. In particular, the proposed approach leverages formal techniques to analyze the key and state space of a sequential circuit to evaluate the security against optimization-based attacks. The experimental evaluation validates that the proposed scheme unveils weaknesses of the protection structure, which remain undetected when using existing techniques.

High-level performance estimation using Machine Learning (ML) can significantly facilitate the exploration of a wide range of processor microarchitecture solutions at the early stage. Moreover, for the selected microarchitecture, it can remarkably accelerate the software optimization step. Recently, ML has been successfully applied to estimate performance, in particular the clock cycles, for various microarchitecture implementations. However, this is clearly not sufficient as the modern processor microarchitectures are complex and require deeper insights into microarchitectural behaviors for better high performance estimation. In this context, finding an accurate and fast approach that can support performance estimation of various microarchitecture implementations of RISC-V Instruction Set Architecture (ISA) is very challenging. In this paper, we go beyond performance estimation based on clock cycles, i.e., we expand on ML techniques to estimate microarchitectural behaviors. We propose a novel approach based on ML to estimate the performance of embedded software on RISC-V processors across different microarchitectures. Our approach leverages a fast functional simulator, cycle-accurate Register Transfer Level (RTL) implementations, and ML techniques to generate Predictive Models (PMs) that provide accurate performance estimation while maintaining fast simulation time. In addition to measuring the clock cycles, we also provide insights into the microarchitectural behavior of different microarchitectures by estimating cache misses/hits, branch prediction behavior, and memory dependencies. Experimental results on four real-world cycle-accurate implementations of RISC-V ISA with different microarchitectures at RTL show that using the proposed approach leads to a huge performance boost up to$\mathbf{2261.4}\times$compared to RTL simulations with an average prediction error 0.4%.

The high-volume manufacturing test ensures the production of defect-free devices, which is of utmost importance when dealing with safety-critical systems. Such a high-quality test requires a deliberately designed scan network to provide a time and cost-effective access to many on-chip components, as included in state-of-the-art chip designs. The IEEE 1687 Std. (IJTAG) has been introduced to tackle this challenge by adding programmable components that enables the design of reconfigurable scan networks. Although these networks reduce the test time by shortening the scan chains’ lengths, the reconfiguration process itself incurs an additional time overhead. This paper proposes a heuristic method for designing customized multi-power domain reconfigurable scan networks with a minimized overall reconfiguration time. More precisely, the proposed method exploits a-priori given non-functional properties of the system, such as the power characteristics and the instruments’ access requirements. For the first time, these non-functional properties are considered to synthesize a well-adjusted and highly efficient multi-power domain network. The experimental results show a considerable improvement over the reported benchmark networks.

Today, Integrated Circuits (ICs) manufactoring is distributed over various foundries, resulting in untrustworthy supply chains. Therefore, significant concerns about malicious intentions like intellectual property piracy of the fabricated ICs exist. Logic Locking (LL) is one well-known protection technique to improve the security of ICs. However, there are approaches to unlocking the circuit, like the SAT-based attack. Significant research has been done on thwarting the SAT-based attack by providing SAT-resilient LL. Nevertheless, these SAT-resilient LL approaches have an inherent structural footprint, yielding a high vulnerability to structural attacks. Recently, Polymorphic Logic Gates (PLGs) have been utilized to implement logic obfuscation by replacing gates. Reconfigurable Field Effect Transistors (RFETs) are a new emerging technology for implementing such PLGs due to their inherent camouflaging properties. This work proposes a novel technique for increasing SAT-resilience while introducing no structural weakness using those PLGs. In particular, based on the concept of an SAT-based attack, a procedure for determining the most SAT-resilient placement of LL-cells is developed. The experimental evaluation proves that the proposed hardening of the placement increases the SAT-resilience compared to a random placement while providing inherent camouflaging of RFET-cells.

RISC-V has generated a lot of interest in academia and industry alike due to the open source, modular, and royalty-free design of the Instruction Set Architecture (ISA). With its modular extensibility and the ability to customize the ISA to meet application-specific needs, new challenges arise in terms of verification. Various approaches have been proposed to overcome these challenges, including traditional simulation-based verification and formal verification. While formal verification is considered thorough, its quality heavily depends on the properties and assumptions of the proofs meeting the exact specification. In this paper, we propose a structured and mutation-based approach for qualifying formal verification techniques related to the RISC-VISA. Specifically, we identify rules and mutation classes that can be used to derive a set of mutations to test the capabilities of formal verification tools. We evaluate our approach through a case study, applying a set of mutations to an open-source RISC-V processor, which we verify using the riscv-formal formal verification framework. Our results identify verification gaps uncovered through the generated mutations. We discuss the impact of these identified gaps and how they can be assessed within the context of formal verification.

General-Purpose Computation on Graphics Processing Units (GPGPUs) are becoming crucial in accelerating computing capacity. Due to the massive parallelism capabilities of GPUs, they can achieve impressive speedups of up to 32 times compared to common CPUs. However, writing highly parallel code and utilizing a GPU is challenging for programmers. Developers are facing new challenges since GPUs handle threads and parallelism differently from CPUs. Academia and industry proposed several profilers to support developers in terms of code optimization. These profilers often require an actual device (e.g., GPU) and take a long time for the profiling process. We propose HyPA, a hybrid Parallel Thread Execution (PTX) Analyzer that inspects PTX code statically and dynamically. HyPA implements a partly functional emulator that executes instructions that rely on runtime dependencies to count the number of executed PTX instructions and divergent branches. HyPa executes compiled kernels—the programs that run on GPUs—generated by the CUDA compiler and supports the full PTX 7.7 specification. Our functional emulator allows significantly faster analysis of PTX code compared to standard profilers. In our evaluation, we quantify this increase in performance through benchmark runs. HyPA achieved speedups of up to 536% compared to the nvprof profiler. Moreover, our approach can gather performance metrics beyond static analysis (e.g., branch efficiency) by a faster execution time than by profiling the application on an actual device. Finally, we provide an open-source implementation of HyPA to help developers and system designers in further research and development.

The development process for new embedded systems relies increasingly on simulation, e.g. to develop hardware and software components in parallel using virtual prototyping. The central component of a virtual prototype is the instruction set simulator (ISS) which implements instruction execution for a specific instruction set architecture (ISA). To avoid erroneous behavior during software simulation, it is paramount to ensure that the provided ISS implements the ISA exactly as specified, i.e. that there are no discrepancies between the hardware and the VP. In order to increase confidence in the correctness of the VP's ISS, it is advantageous to generate it automatically from a formal model of the ISA instead of implementing it manually. While a variety of formal ISA models have been proposed in prior work, they are presently not widely used in the VP domain. We attempt to ease employment of formal models for ISS generation in this domain. To this end, we reduce the integration effort through a simulator-agnostic ISS generation approach that integrates well with existing simulators and existing vendor-supplied VP components. Our approach leverages a formal RISC-V ISA model which exclusively describes instruction semantics and abstracts interactions with hardware components through an interface model, thus encapsulating interactions with simulator-specific code. As part of our experiments, we were able to generate an ISS for the popular RISC-V implementations Spike and RISC-V VP, thereby replacing their manually written implementations. Performed benchmarks indicate that the generated ISS offers the same simulation performance as a manually written one, while still passing the official RISC-V tests.

Most hardware in the area of IoT and embedded systems only ever runs a single application. To reduce the cost and increase performance the hardware can be tailored to this application. Unfortunately, identifying, designing, and evaluating application-specific optimizations is complex and requires significant effort. However, application-specific hardware also performs significantly better compared to using general-purpose processors. Prior work attempts to address this problem via approaches from the Register-Transfer Level (RTL) as well as the application level, with RTL being effective but resource-intensive, while high-level approaches are faster but lack accuracy. In order to combine the advantages of high-level and low-level approaches we propose an open source Virtual Prototype (VP) based workflow to automatically identify promising hardware optimization candidates based on recurring patterns. Our results demonstrate that a VP can be used effectively as a starting point for application-specific hardware optimization.

Only formal methods can guarantee the correctness of a circuit, but are usually very time and memory consuming. Therefore, efficient formal verification is key in the design of complex circuits. Many verification techniques have been introduced, which mostly fail to give bounds for the time complexity of the verification process. To overcome this issue, Polynomial Formal Verification (PFV) was introduced. This paper introduces a novel approach to PFV of circuits, by leveraging the concept of constant cutwidth. We divide the circuit into subgraphs, one for every output. This makes the verification of every subgraph only dependent on the cutwidth of the circuit and independent of the bitwidth. One main problem we solve is the passing of information between those subgraphs. The approach enables formal verification in linear time for circuits with constant cutwidth.

IoT devices offer insufficient protections against exploitation of critical programming errors (such as buffer overflows) it is therefore paramount to sufficiently test IoT software before deployment. A central source of these errors is the implementations of stateful network protocols used in the IoT (e.g., MQTT-SN). Unfortunately, comprehensive automated testing of such protocol implementations is challenging due to their large state space. Furthermore, prior work on automated testing of protocol implementations focuses on conventional desktop systems and does thus not address challenges specific to the IoT domain (e.g., handling of peripheral interactions). In this publication, we leverage symbolic execution (an automated software testing technique) for testing stateful network protocol implementation in the IoT domain. To mitigate issues regarding the state-space explosion, we propose a novel symbolic execution approach which is based on created protocol state and message format specifications and specifically tailored to the IoT domain. We employ our specification-based symbolic execution approach to test protocol implementations provided by two popular IoT operating systems. Our experiments indicate that a significant increase in code coverage can be achieved using our automated software testing approach. We were further able to discover three critical and previously unknown bugs in network protocol implementations provided by the RIOT operating system.

Laser-assisted side-channel analysis techniques, such as optical probing (OP), have been shown to pose a severe threat to secure hardware. While several countermeasures have been proposed in the literature, they can either be bypassed by an attacker or require a modification in the transistor's fabrication process, which is costly and complex. In this work, firstly, we propose a formulation for the caliber of reflected light from OP. Secondly, we propose circuit design techniques and logic styles to alleviate OP attacks based on our formulation. Finally, we compare several logic families and circuit design techniques in terms of performance and OP security merits. In this regard, we perform simulations to compare the optical beam interaction between the different logic gates. By utilizing our proposed circuit design techniques and dual-rail logic (DRL), the signal-to-noise ratio (SNR) of the reflected light from OP is reduced significantly.

Software written for constrained devices, commonly used in the Internet of Things (IoT), is primarily written in C and thus subject to vulnerabilities caused by the lack of memory safety (e.g. buffer overflows). To prevent these vulnerabilities, we present a systematic approach for finding spatial memory safety violations in low-level code for constrained embedded devices. We propose implementing this approach using SystemC-based Virtual Prototypes (VPs) and illustrate an architecture for a non-intrusive integration into an existing VP. To the best of our knowledge, this approach is novel as it is the first for finding spatial memory safety violations which addresses challenges spe-cific to constrained devices. Namely, limited computing resources and utilization of custom hardware peripherals. We evaluate our approach by applying it to the IoT operating system RIOT where we discovered seven previously unknown spatial memory safety violations in the network stack of the operating system.

Evolutionary algorithms are a well-known optimisation technique, especially for non-convex, multi-modal optimisation problems. Their capability of adjusting to different search spaces and tasks by choosing the suitable encoding and operators has led to their widespread use in various application domains. However, application domains sometimes come with difficulties like fitness functions that can not be evaluated or not more than a few times. In these situations, surrogate functions or approximative fitness functions allow the evolutionary algorithm to work despite this complication. Still, using approximative fitness functions comes with a price: The fitness value is no longer correct for every individual, and the algorithm can not know which value to trust. However, statistical methods yield knowledge about the preciseness of the approximation. We propose using this knowledge to adapt the fitness value to ease the effects of the approximative nature. We choose to use the information given in the density of the training data, which has computational merits over the use of other techniques like cross-validation or prediction intervals. We evaluate our method on four well-known benchmark functions and achieve good optimisation success and computation time results.

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.

We propose a novel cross-level verification approach for processor verification at the Register-Transfer Level (RTL). The foundation is a randomized coverage-guided instruction stream generator that produces one endless and unrestricted instruction stream that evolves dynamically at runtime. We lever-age an Instruction Set Simulator (ISS) as a reference model in a tight co-simulation setting. Coverage information is continuously updated based on the execution state of the ISS and we employ Coverage-guided Aging to smooth out the coverage distribution of the randomized instruction stream over the time. In combination, this enables a broad and deep coverage to find intricate corner-case bugs in the RTL processor. Our case study with an industrial pipelined 32 bit RISC- V processor demonstrate the effectiveness of our approach.

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

HDLs are widely used in EDA for abstract specification and synthesis of logic circuits. Despite the popularity and the many benefits of HDL-based synthesis, it has not yet been performed for in-memory computing. Hence, there is a need to design a particular HDL which supplies efficient and compatible descriptions. In this paper, we enable HDL-based synthesis for the Programmable Logic-in-Memory (PLiM) computer architecture. We present LiM-HDL - a Verilog-based HDL - which allows for the detailed description of programs for in-memory computation. Having the description given in LiM-HDL, we propose a synthesis scheme which translates the description into PLiM programs, i.e. a sequence of resistive majority operations. This includes lexical and syntax analysis as well as preprocessing, custom levelization and a compiler. In our experiments, we show the benefits of LiM-HDL compared to classical Verilog-based synthesis. We show in a case-study that LiM-HDL can be used to implement programs with respect to constraints of specific applications such as edge computing in IoT, for which the PLiM computer is of particular interest and where low area is a key requirement. In our case-study, we show that we can reduce the number of ReRAM devices needed for the computation of an encryption module by 69%.

Due to the increasing complexity of analog circuits and their integration into System-on-Chips (SoC), the analog design and verification industry would greatly benefit from an expansion of system-level methodologies, which provide speed benefits in comparison to SPICE simulations and allow interoperability with digital tools at the system-level. However, a key barrier to the expansion of system-level tools for analog circuits is the lack of confidence in system-level models implemented in SystemC AMS. To overcome this, functional equivalence of system-level models to respective SPICE-level models needs to be demonstrated. In this paper, we develop a novel, graph-based methodology to formally check equivalence between system-level and SPICE-level representations of linear analog filter circuits, such as Low-Pass Filters (LPF). To do this, we propose an intermediate representation in the form of a Signal-flow Graph (SFG), which acts as a mapping function from the SPICE-level to the system-level. We create the intermediate representation with linear graph modeling from the SPICE-level model and use graph manipulation to transform the intermediate representation to the equivalent system-level model. We demonstrate the applicability of the proposed methodology by successfully applying it to two example filters.

With the growing demands for highly area-efficient, delay-optimized, and low-power designs, the complexity of digital circuits is increasing as well. Especially, a wide variety of arithmetic circuits, including different types of adders, multipliers, and dividers have been proposed to meet the demands in applications such as cryptography and Artificial Intelligence (AI). Some of these arithmetic circuits have highly parallel architectures and contain millions of gates; as a result, they are extremely error-prone. In the last 30 years, several formal verification methods have been proposed to verify arithmetic circuits. These methods report very good results when it comes to the verification of adders and structurally simple multipliers. Moreover, their space and time complexities are polynomial, i.e, they are scalable. However, when it comes to the verification of structurally complex multipliers, the story is different.In this paper, we investigate the space and time complexity of verifying a structurally complex multiplier using a word-level verification method. We prove that the space and time complexity is always exponential. Then, we introduce a new verification strategy that takes advantage of several verification engines. We show that the polynomial formal verification of the complex multiplier becomes possible if the correctness of each stage is verified using the proper verification method. Our verification strategy can be applied to other complex digital circuits.

RISC-V is a modern open source Instruction Set Architecture (ISA) and designed in a very extendable manner, which allows for highly application specific solutions. However, the identification of suitable instruction set extensions usually requires a significant manual effort and therefore is a very challenging process. In this paper we propose a lightweight alternative methodology to find suitable application-specific RISC-V extensions, using a Virtual Prototype (VP). This is done, purely by observing the used instructions during the execution of the targeted application on the VP. Therefore, no further information about the application itself are needed. In this context the advantages and the flexibility of a VP and the straightforward extendability of the RISC-V ISA are demonstrated.

The increasing application of Machine Learning (ML) techniques on the Internet of Things (IoTs) has led to the leverage of ML accelerators like General Purpose Computing on Graphics Processing Units (GPGPUs) in such devices. However, selecting the most appropriate accelerator for IoT devices is very challenging as they commonly have tight constraints e.g., low power consumption, latency, and cost of the final product. Hence, the design of such application-specific IoT devices becomes a time-consuming and effort-hungry process, that poses the need for accurate and effective automated assisting methods.In this paper, we present a novel approach to estimate the power consumption of CUDA-based Convolutional Neural Networks (CNNs) on GPGPUs in the early design phases. The proposed approach takes advantage of a hybrid technique where static analysis is used for features extraction and the K-Nearest Neighbor (K-NN) regression analysis is utilized for power estimation model generation. Using K-NN analysis, the power estimation model can even be created with small training datasets. Experimental results demonstrate that the proposed approach is able to predict CNNs power consumption up to a Absolute Percentage Error of 0.0003% in comparison to the real hardware.

RISC-V-based embedded systems are becoming more and more popular in recent years. Performance estimation of embedded software at an early stage of the design process plays an important role in efficient design space exploration and reducing time-to-market constraints. Although several cycle-accurate RISC-V simulators at different levels of abstraction have been proposed, they have an inherently high cost, both for the development of the simulation setting and for obtaining the software performance in terms of the number of cycles through simulation. This results in a significant burden on designers to perform design space exploration.In this paper, we present a novel ML-based approach, enabling designers to fast and accurately estimate the performance of a given embedded software implemented on the RISC-V processor at the early stage of the design process. The proposed approach is evaluated against a real-world cycle-accurate RISC-V Virtual Prototype (VP) using a set of standard benchmarks. Our experiments demonstrate that our approach allows obtaining highly-accurate performance estimation results in a short execution time. In comparison to the cycle-accurate RISC-V VP model, the proposed approach achieves up to more than 5 x faster simulation speed and less than 2.5% prediction error on average.

Heterogeneous platforms, that integrate CPU and FPGA-based processing units, are emerging as a promising solution for accelerating various applications in the embedded system domain. However, in this context, so far, comprehensive studies that combine theoretical features of real-time task scheduling with practical runtime architectural characteristics have mostly been ignored. To fill this gap, in this paper we propose a real-time scheduling algorithm with the objective of minimizing the overall execution time under hardware resource constraints for heterogeneous CPU+FPGA architectures. In particular, we propose an Integer Linear Programming (ILP) based technique for task allocation and scheduling. We then show how to implement a given scheduling on a practical CPU+FPGA system regarding current technology restrictions and validate our methodology using a practical RISC-V case-study. Our experiments demonstrate that performance gains of 40 % and area usage reductions of 67 % are possible compared to a full software and hardware execution, respectively.

Memristors or Resistive Random Access Memory (RRAM) are emerging non-volatile memory devices that can be used for both storage and computing. In this type of memory the information is stored in memory cells in the form of resistance. One of the very important challenges in memristive crossbars is the existence of Sneak Paths, which result in erroneous reading of memory cells. Most of the logic in-memory techniques have emphasized on improving the logic design perspective, but have given minor importance to the sneak path issue. In this paper we show the effect of sneak paths on crossbars of various sizes, and then try to analyze the logic design approaches like MAGIC and MAJORITY with respect to their immunity to sneak paths. Experimental result shows that with some extra overhead we can eliminate the sneak path effect in various logic design methods.

In order to overcome the von Neumann bottleneck, recently the paradigm of in-memory computing has emerged. Here, instead of transferring data from the memory to the CPU for computation, the computation is directly performed within the memory. ReRAM, a resistance-based storage device, is a promising technology for this paradigm. Based on ReRAM, the PLiM computer architecture and LiM-HDL, an HDL for specifying PLiM programs have emerged. In this paper, we first present a novel levelization algorithm for LiM-HDL. Based on this novel algorithm, large circuits can be compiled to PLiM programs. Then, we present a verification scheme for these programs. This scheme is separated into two steps: (1) A proof of purity and (2) a proof of equivalence. Finally, in the experiments, we first apply our levelization algorithms to a well-known benchmark set, where we show that we can generate PLiM programs for large benchmarks, for which existing levelization algorithms fails. Then, we apply our proposed verification scheme to these PLiM programs.

The problem of synthesis and optimization of reversible and quantum circuits have drawn the attention of researchers for the last two decades due to increasing interest in quantum computing. Although lot of works have been done on the synthesis of binary reversible circuits, very less works have been reported on the synthesis of ternary reversible circuits. Ternary circuits have lower cost of implementation as compared to their binary counterparts. However, the synthesis approaches that exist for ternary reversible circuits either use too many circuit lines (qutrits) or too many gates. Only one prior work has discussed the problem of generating cost-optimal ternary reversible circuits, but for a very restrictive gate library, which limits the approach to a specific subset of ternary reversible functions and often the solution becomes sub-optimal due to the imposed restrictions. The present paper overcomes that restriction, and uses multiple control ternary Toffoli gates with all possible ternary target operations as the gate library. This gate library is functionally complete and can be used to synthesize any arbitrary function. The proposed SAT-based synthesis approach provides low cost solutions in terms of the number of gates for any arbitrary ternary reversible function. Experimental results on various randomly generated permutations as well as standard ternary benchmarks establish this claim. The results can be used as template for other synthesis approaches by observing how far they deviate from the optimal solutions.

To ensure the functional correctness of digital circuits, formal verification methods have been established, where the circuits are proven to implement the correct function. Several methods exist for the execution of the verification process. However, the verification process can have an exponential time or space complexity, causing the verification to fail. While exponen-tial in general, recently it has been proven that the verification complexity of several circuits is polynomially bounded. In this paper, we prove the polynomial verifiability of several state-of-the-art approximate adders using BDDs. These approx-imate adders include handcrafted approximate adders, which consist of several subadders, as well as automatically generated approximate adders, where regular adders can be arbitrarily altered by removing gates and changing the type of gates. Thus, this paper provides insight into the possible methods for the design of approximate adders, such that the approximate adders remain polynomially verifiable. Here, we give upper bounds for the BDD sizes during the verification process, as well as for the time and space complexity. The upper bounds for the BDD sizes are then experimentally evaluated.

The high distribution of the manufacturing of Integrated Circuits (ICs) over different foundries yields long and untrustworthy supply chains. Logic locking is one prominent protection technique against malicious usage and counterfeit. The emerging technology of Reconfigurable Field-Effect Transistors (RFETs) has recently been utilized to implement new polymorphic logic mechanisms to protect intellectual property. The mechanisms’ assessment is important to reinforce the newly introduced protection mechanism and, hence, avoid any weak logic structures. So far, approximate Hamming Distance-based assessment techniques have been used for determining the protection quality while considering combinatorial circuits only. This work proposes a novel method to assess the quality of the RFET-based logic locking structures for sequential circuits. In particular, formal techniques are orchestrated to analyze the circuit’s state space to determine whether any incorrect keys exist that unintentionally unlock and exhibit the circuit’s correct functional behavior. The experimental evaluation validates that the proposed scheme unveils weaknesses of the protection structure, which remain undetected when using existing techniques.

Coverage-guided Fuzzing (CGF) has been shown to be a very effective verification technique in the Software (SW) domain. However, the application of CGF in the embedded system domain is much more limited so far. Beside the necessary integration effort of the fuzzing engine, a main limiting factor is the employed coverage metric to guide the CGF process. Since embedded systems integrate Hardware (HW) and SW parts, the coverage metric should reflect both parts instead of reasoning exclusively about the SW execution in the CGF process.Therefore, in this paper, we propose a novel unified HW/SW coverage metric to boost state-of-the-art CGF for HW/SW co-verification. Following the modern design flow for embedded systems, we leverage a Virtual Prototype (VP) to represent the HW part. We designed effective representations of the unified HW/SW coverage to capture all relevant coverage information at run time in the VP and tailored it for integration with a modern CGF process. Our RISC-V experiments demonstrate the practical applicability of our proposed approach. Our proposed unified HW/SW coverage can be effectively managed at runtime and enables to reach deeper bugs compared to existing state-of-the-art CGF.

The demand for AI and specifically machine learning functionality on edge devices (TinyML) is growing. TinyML faces several unique challenges, one of them being the requirement of having a lower memory footprint for storage and inference of neural networks.In this paper, we propose and evaluate an approach to make Convolutional Neural Networks (CNNs) with higher memory footprint executable on edge devices. The idea is to combine flash memory with a cached access for the inference of CNNs. In order to evaluate the effectiveness of our proposed memory architecture by measuring the cache hitrate at the system level, we build a Virtual Prototype (VP) with a dedicated flash device and an exclusive cache. We are using Tensorflow Lite Micro (TFLM) for the network inference and mapping all model data and runtime buffers into the cache enhanced flash memory. Multiple experiments with several cache configurations show that a small cache of around 1 KB is able to achieve very high hitrates over 99%. Additionally, the experimental results show that the memory planning of TFLM supports the usage of caching because most memory accesses are adjacent.

Symbolic execution is a powerful software testing technique for finding bugs in complex software. Unfortunately, following the symbolic execution and understanding its results is challenging. However, since symbolic execution is commonly not complete (i.e. due to path explosion) it is important to understand the limitations of the performed analysis. Otherwise, insufficiently tested code parts may not be identified and bugs remain unnoticed. Prior work attempts to address this problem via 2D visualizations which communicate properties of the performed analysis to the verification engineer. Since symbolic execution requires a visualization of several properties, such 2D visualizations often lack important information or end up being dense and difficult to understand.In order to overcome this limitation, we propose a novel 3D visualization of symbolic execution which allows visualizing additional properties via the third dimension. For this purpose, we have implemented a 3D visualization for the symbolic execution of RISC-V machine code and evaluate this implementation by comparing it to an existing 2D visualization. Our results demonstrate that the third dimension allows us to include additional information which is not captured by the existing 2D visualization. In order to stimulate further research on 3D visualization of symbolic execution, we have released our implementation as open source software.

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.

RISC-V is a modern Instruction Set Architecture (ISA) that by its open nature in combination with a clean and modular design has enormous potential to become a game changer in the Internet of Things (IoT) era. Recently, SystemC-based Virtual Prototypes (VPs) have been introduced into the RISC-V ecosystem to lay the foundation for advanced industry-proven system-level use-cases. However, a VP-driven environment modeling and interaction has been mostly neglected in the RISC-V context.

Recently, a lot of effort has been put into developing formal verification approaches by both academic and industrial research. In practice, these techniques often give satisfying results for some types of circuits, while they fail for others. A major challenge in this domain is that the verification techniques suffer from unpredictability in their performance. The only way to overcome this challenge is the calculation of bounds for the space and time complexities. If a verification method has polynomial space and time complexities, scalability can be guaranteed.

The integration of Design for Testability measures is strictly required when designing complex Integrated Circuits (ICs) to ensure that a good testability prevails in the resulting design. By this, a high-quality manufacturing test can be performed, giving a certain level of confidence that no defects have occurred during the manufacturing process, which potentially tamper with the functional behavior's correctness. However, a high-quality test implies large test data volume and high test application time, yielding high test costs. This effect is even more amplified when testing ICs for safety-critical applications like automotive systems or avionics, enforcing a zero-defect policy. Analogously, specific structures for the Design for Debug and Diagnosis are introduced since similar problems exist when debugging complex systems. Finally, the Design for Reliability is becoming increasingly important in applications like avionics since the introduced system has typically to deal with harsh environmental conditions and, hence, the IC has to exhibit a specific level of robustness to withstand. This paper proposes novel contributions to, in the end, pave the way for the next generation of IC, which can be successfully and reliably integrated even in safety-critical applications. In particular, this paper combines formal techniques, such as the Boolean satisfiability problem and bounded model checking, to propose (I) a novel test access mechanism with embedded compression including an optimization-based retargeting framework, (II) a new hybrid compression architecture to address compression aborts and (II) an effective fault detection mechanism for single transient faults. The proposed measures are evaluated by considering industrial-relevant benchmark candidates, demonstrating their effectiveness and showing that state-of-the-art techniques are outperformed.

The demand for optimized and efficient embedded software is increasing in many applications such as the Internet of Things (IoT) or other Cyber-Physical Systems (CPS). Hence, early performance analysis of embedded software is essential to perform Design Space Exploration (DSE), ensure efficiency, and meet time-to-market constraints. Designers usually use real hardware, simulators, or static analyzers to obtain the performance. However, these methods suffer from serious drawbacks as real hardware is not available in the early stage of the design process, simulators either do not support any timing accuracy or require large execution time, and static analyzers need details of the hardware microarchitecture. In this paper, we present a novel Artificial Neural Network (ANN)-based approach that allows a fast and accurate performance estimation of embedded software for RISC-V processors in the early design phases. This can significantly reduce the burden on designers to perform DSE. The proposed approach takes advantage of the dynamic analysis technique and analytical models and does not require any microarchitecture-related parameters such as cache misses, cache hits, and memory-level parallelism. We compare our proposed microarchitecture-independent approach with state-of-the-art in terms of speed and accuracy. Our experiments on various benchmarks demonstrate that the proposed approach achieves a speed-up of$4.41\times$compared to a RISC-V Virtual Prototype (VP) at the Electronic System Level (ESL), while the estimation results have only a Mean Absolute Percentage Error (MAPE) of 2%.

Memristor-based crossbar architectures have been explored by researchers for neuromorphic computing, where analog vector-matrix multiplication can be carried out in a single time step. In this paper we explore such architectures for carrying out various arithmetic operations. Since the computations are carried out in analog domain, they are affected by fabrication and performance variability of the manufactured devices. As a result, there can be inherent errors during the computation. However, the architecture can be suitable for approximate computing applications where some errors can be tolerated. We have proposed a method for carrying out arithmetic operations with any multiple of k-bit resolution on the crossbar, for some limited values of k. The fault tolerant capability of the proposed architecture is evaluated through experimentation on benchmark datasets. We also perform case studies to analyze the performance of the approach with particular emphasis on approximate computing. The results of the case studies show that certain applications indeed exhibit fault tolerance in presence of faulty memristors.

With the growing complexity of digital circuits, formal verification has become a crucial task after the design in order to ensure the correctness of a circuit. Many existing verification methods suffer from unpredictability in their performance. It is not clear whether they have to be run for seconds, hours, or days to return the verification results or whether they fail in the end. The unpredictability can only be resolved by ensuring complexity bounds. To guarantee scalability we are in particular interested in Polynomial Formal Verification (PFV), where the space and time complexities have polynomial bounds with respect to the size of the circuit.The information about the design hierarchy is usually vital for PFV. Complex digital circuits consist of several components that cannot be verified with an individual verification technique in polynomial space and time. However, with additional knowledge about the boundaries of components, PFV becomes possible through the step-wise verification of sub-components and the use of different formal proof engines. In this paper, we first introduce PFV and clarify its importance. We consider the verification of several flattened gate-level arithmetic circuits and illustrate the challenges of PFV when no design hierarchy is available. Then, we show how these challenges can be overcome by preserving design hierarchy information including the boundaries of the components.

Over the last years, the structure sizes of integrated circuits have significantly been decreased. This allows for the development of small, powerful, and energy-efficient circuits, as required for the challenging application scenarios like given in automotive or avionic systems. Nanometer scaled technology nodes are more vulnerable against transient faults, for instance, as induced by high radiation beams, potentially causing an erroneous behavior of the system. Different types of approaches have been proposed to increase the robustness of circuits against these faults, particularly for safety-critical applications. Such a countermeasure calculates, for instance, application-specific knowledge yielding a highly efficient fault detection mechanism that enhances the robustness significantly. Since these approaches invoke formal techniques for an advanced state analysis, a high computational effort is required, limiting the applicability for large circuit designs. This work addresses these shortcomings by combining an evolutionary algorithm with newly developed multi-objective optimization operators, deliberately designed for the state analysis of sequential circuits. The developed measures are all seamlessly integrated into one dedicated hardware module. By this, prototyping devices like field programmable gate arrays can be orchestrated during the regular circuit design flow to execute the proposed module to, in the end, benefit from an enormous hardware-acceleration. The experimental evaluation clearly proves that the presented method allows calculating application-specific knowledge effectively. More precisely, the run-time is reduced by more than 1,200X while retaining (or even improving) the efficacy of the resulting on-chip fault detection mechanism compared to state-of-the-art in terms of robustness enhancement and introduced hardware overhead.

Abstract Virtual prototypes (VPs) are crucial in today’s design flow. VPs are predominantly created in SystemC transaction-level modeling (TLM) and are leveraged for early software development and other system-level use cases. Recently, virtual prototyping has been introduced for the emerging RISC-V instruction set architecture (ISA) and become an important piece of the growing RISC-V ecosystem. In this paper, we present enhanced virtual prototyping solutions tailored for RISC-V. The foundation is an advanced open source RISC-V VP implemented in SystemC TLM and designed as a configurable and extensible platform. It scales from small bare-metal systems to large multi-core systems that run applications on top of the Linux operating system. Based on the RISC-V VP, this paper also discusses advanced VP-based verification approaches and open challenges. In combination, we provide for the first time an integrated and unified overview and perspective on advanced virtual prototyping for RISC-V.

Resistive Random Access Memory (ReRAM) is an emerging non-volatile memory technology. Besides its low power consumption and its high scalability, its inherent computation capabilities make ReRAM especially interesting for future computer architectures. Merging computations into the memory is a promising solution for overcoming the memory bottleneck. To perform computations in ReRAM, efficient synthesis strategies for Boolean functions have to be developed. In this article, we give a thorough presentation of how to employ parallel computing capabilities of ReRAM for the synthesis of functions given state-of-the-art graph-based representations AIGs or BDDs. Additionally, we introduce a new graph-based representation called m-And-Inverter Graph (m-AIGs), which allows us to fully exploit the computing capabilities of ReRAM. In the simulations, we show that our proposed approaches outperform state-of-the art synthesis strategies, and we show the superiority of m-AIGs over the standard AIG representation for ReRAM-based synthesis.

No abstract available.

In this paper we propose μ RV32 (MicroRV32) an open source RISC-V platform for education and research. μ RV32 integrates several peripherals alongside a configurable 32 bit RISC-V core interconnected with a generic bus system. It supports bare-metal applications as well as the FreeRTOS operating system. Beside an RTL implementation in the modern SpinalHDL language ( μ RV32 RTL) we also provide a corresponding binary compatible Virtual Prototype (VP) that is implemented in standard compliant SystemC TLM ( μ RV32 VP). In combination the VP and RTL descriptions pave the way for advanced cross-level methodologies in the RISC-V context. Moreover, based on a readily available open source tool flow, μ RV32 RTL can be exported into a Verilog description and simulated with the Verilator tool or synthesized onto an FPGA. The tool flow is very accessible and fully supported under Linux. As part of our experiments we provide a set of ready to use application benchmarks and report execution performance results of μ RV32 at the RTL, VP and FPGA level together with a proof-of-concept FPGA synthesis statistic for different processor configurations. We believe that our μ RV32 platform is a suitable foundation for further research and education purposes due to its open source nature, accessible toolchain working in Linux and support for small low-priced FPGAs in combination with a solid feature set.

Constrained Internet of Things (IoT) devices with limited computing resource are increasingly employed in security critical areas. Therefore, it is important for the firmware of these devices to be tested sufficiently. On non-constrained conventional devices, dynamic testing techniques (e.g. fuzzing, symbolic execution, or concolic testing) are successfully utilized to discover critical bugs in tested software. Unfortunately, the diverse ecosystem and the dependence on low-level details of a wide range of peripherals makes it difficult to use these techniques in the IoT context. In order to address these challenges, we present SymEx-VP an open source emulation-based approach for concolic testing of IoT firmware. SymEx-VP is a virtual prototype for RISC-V hardware platforms and allows concolic testing of RISC-V machine code. To support a wide range of different peripherals, SymEx-VP utilizes SystemC, a hardware modeling language for C++. By employing a SystemC extension mechanism, SymEx-VP can inject concolic inputs into the emulated firmware through the memory-mapped I/O peripheral interface of existing SystemC peripheral models. This allows us to support different operating systems and libraries used in the IoT with minimal integration effort. We provide an extensive description of SymEx-VP, illustrate peripheral modeling and firmware testing using it by example, and perform tests with four operating systems to demonstrate the advantages of our OS-agnostic firmware testing method.

The emergence of virtual prototypes (VPs) at the electronic system level (ESL) has played a major role in modernizing the system-on-chips (SoCs) design process to raise design productivity and reduce time-to-market. A VP is an abstract and executable software model implemented typically using SystemC and its transaction-level modeling (TLM) framework. However, this modern VP-based design process still has weaknesses, in particular, due to the significant manual effort involved for design understanding, analysis, and modeling tasks which is both time consuming and error-prone. This article introduces an automated and fast design understanding approach that enables designers to trace detailed information of the VPs’ structure and behavior. Experimental results including a real-world VP-based SoC show the advantages of our approach, such as its accuracy, applicability, and scalability.

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.

In order to meet the time-to-market constraint, High-level Synthesis (HLS) is being increasingly adopted by the semiconductor industry. HLS designs, which can be automatically translated into the Register Transfer Level (RTL), are typically written in SystemC at the Electronic System Level (ESL). Timing-based information leakage and its countermeasures, while well-known at RTL and below, have not been yet considered for HLS. The paper makes a contribution to this emerging research area by proposing ATLaS, a novel timing-based information leakage flows detection approach for SystemC HLS designs. The efficiency of our approach in identifying timing channels for SystemC HLS designs is demonstrated on two security-critical architectures which are shared interconnect and crypto core.

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.

Field-coupled Nanocomputing (FCN) is a class of post-CMOS emerging technologies, which promises to overcome certain physical limitations of conventional solutions such as CMOS by allowing for high computational throughput with low power dissipation. Despite their promises, the design of corresponding FCN circuits is still in its infancy. In fact, state-of-the-art solutions still heavily rely on conventional synthesis approaches that do not take the tight physical constraints of FCN circuits (particularly with respect to routability and clocking) into account. Instead, physical design is conducted in a second step in which a classical logic network is mapped onto an FCN layout. Using this two-stage approach with a classical and FCN-oblivious logic network as an intermediate result, frequently leads to substantial quality loss or completely impractical results. In this work, we propose a one-pass synthesis scheme for FCN circuits, which conducts both steps, synthesis and physical design, in a single run. For the first time, this allows to generate exact, i. e., minimal FCN circuits for a given functionality.

Nowadays, prefix adders are widely used in different designs and applications due to their flexible carry propagation hardware. The variety of these adders makes it possible to find the best choice based on the design parameters, e.g., area, delay, number of wiring tracks. Proving the correctness of prefix adders is an important task after their design as they usually have a complex and error-prone structure. It has been experimentally shown that Binary Decision Diagrams (BDDs) are very efficient in the formal verification of adders, including prefix adders. However, it has been never proved theoretically. In this paper, we calculate the computational complexity of proving the correctness of prefix adders using BDDs. Based on these calculations, we show that the formal verification of prefix adders can be done in time polynomial in n, where n is the size of the adder (i.e., the number of bits per input). We also compare the theoretical calculations with the experimental results to clarify the differences between the complexities in theory and practice.

Evolutionary algorithms are a successful application of bio-inspired behaviour in the field of Artificial Intelligence. Transferring mechanisms such as selection, mutation, and recombination, evolutionary algorithms are capable of surmounting the disadvantages of traditional methods. Adjusting an evolutionary algorithm to a specific problem requires both, a good understanding of the problem and deep knowledge of the effects of choosing one or another operator in the algorithm. This becomes an especially difficult task when the fitness function is not analytically given - that is, exists only as an approximation, that is highly dependent on the present training data. We propose using prediction intervals to modify the fitness function such, that worse fitness values are less penalized if they occur in a poorly fitted area. We evaluate this with an example from material sciences as well as four standard benchmark algorithms for evolutionary algorithms using a Support Vector Regression for training the approximative fitness function and find that our approach outperforms the naive approximative function.

Evolutionary algorithms are a very general method for optimization problems that allow adaption to many different use cases. Application to real-world problems usually comes with features as constraints, dependencies and approximations. When a multidimensional search space comes with strings attached- namely dependencies between its dimensions- an expression in two ways is possible: Restrictive-as equalities or inequalities- or vague-as correlations between dimensions, for example. Correlations between dimensions are not as easy to grasp as constraints. Therefore, well-known techniques as death penalty or penalty functions do not apply directly. We propose new mutation and recombination operators that incorporate domain knowledge to increase the offspring fraction that adheres to these correlations. We evaluate our approach with several benchmark functions and different assumptions on the dependencies of the search space. We compare the likelihood of valid (in terms of adhering correlations) outcomes of algorithms using standard mutation and recombination operators to those with the proposed operators. We find that the correlation-aware operators preserve population's features in terms of dependencies.

Despite the recent success of formal verification methods, the computational complexity of most of them is still unknown. It raises serious questions regarding the scalability of the approaches. One of the most successful formal methods to prove the correctness of adders is Binary Decision Diagram (BDD)-based verification. It reports very good results for verification of different adder architectures. However, the computational complexity of BDD-based verification has not been yet fully investigated. In this paper, we calculate the complexity of verifying one of the fastest available adders, i.e., conditional sum adder. Then, we show that the verification of this architecture is possible in polynomial time. Finally, we confirm our theoretical calculations by experimental results.

In this paper we propose to combine the safe C dialect Checked C with concolic testing to obtain an effective methodology for attaining safer C code. Checked C is a modern and backward compatible extension to the C programming language which provides facilities for writing memory-safe C code. We utilize incremental conversions of unsafe C software to Checked C. After each increment, we leverage concolic testing, an effective test generation technique, to support the conversion process by searching for newly introduced and existing bugs.Our RISC-V experiments using the RIOT Operating System (OS) demonstrate the effectiveness of our approach. We uncovered 4 previously unknown bugs and 3 bugs accidentally introduced through our conversion process.

Quantum computation received a steadily growing attention in recent years, especially supported by the emergence of publicly available quantum computers like the popular IBM QX series. In order to execute a reversible or quantum circuit on those devices, a mapping is required that replaces each reversible or quantum gate by an equivalent cascade of elementary, i.e. directly executable, gates-a task which tends to induce a significant mapping overhead. Several approaches have been proposed for this task which either rely on the swapping of physically adjacent qubits or the use of precomputed templates, so-called remote CNOT gates. In this paper, we show that combining both, swapping and remote gates, at the reversible circuit level has the prospect of significantly reducing the mapping overhead. We propose a methodology to compute the optimal combination of swaps and templates for Multiple-Controlled Toffoli gates. By using a formulation as a single-source shortest-path problem, a complete database of optimal combinations can be computed efficiently. Experimental results indicate that the mapping overhead can be significantly reduced.

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.

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

With the advent of 5G and IoT applications, there is a greater thrust in terms of hardware security due to imminent risks caused by high amount of intercommunication between various subsystems. Security gaps in integrated circuits, thus represent high risks for both-the manufacturers and the users of electronic systems. Particularly in the domain of Intellectual Property (IP) protection, there is an urgent need to devise security measures at all levels of abstraction so that we can be one step ahead of any kind of adversarial attacks. This work presents IP protection measures from multiple perspectives-from system-level down to device-level security measures, from discussing various attack methods such as reverse engineering and hardware Trojan insertions to proposing new-age protection measures such as multi-valued logic locking and secure information flow tracking. This special session will give a holistic overview at the current state-of-the-art measures and how well we are prepared for the next generation circuits and systems.

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).

We propose an effective methodology for integrating Concolic Testing (CT) with SystemC-based Virtual Prototypes (VPs) for verification of embedded SW binaries. Our methodology involves three steps: 1) integrating CT support with the Instruction Set Simulator (ISS) of the VP, 2) utilizing the standard TLM-2.0 extension mechanism for transporting concolic values alongside generic TLM transactions, and 3) providing lightweight concolic overlays for SystemC-based peripherals that enable non-intrusive CT support for peripherals and thus significantly reduce the CT integration effort. Our RISC-V experiments using the RIOT operating system demonstrate the effectiveness of our approach.

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying verification problem is NP-complete. In this paper we prove that for different types of adder circuits polynomial verification can be ensured based on BDDs. While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process can be carried out in polynomial time. This is shown for the simple Ripple Carry Adder, but also for fast adders like the Conditional Sum Adder and the Carry Look Ahead Adder. Properties about the adder function are proven and the core principle of polynomial verification is described that can also be extended to other classes of functions and circuit realizations.

High-level Synthesis (HLS) using system-level modeling language SystemC at the Electronic System Level (ESL) is being increasingly adopted by the semiconductor industry to raise design productivity. However, errors in the high-level design can propagate down to the low-level implementation and become very costly to fix. Thus, SystemC HLS verification and debugging are necessary and important. While monitoring simulation behavior is a straightforward solution to debug a given design in the case of an error (results of verification), it can become a very time-consuming process as a large amount of data that is not necessarily relevant to the source of error is analyzed.In this paper, we propose a fast and automated debugging-aware visualization approach, enabling designers to monitor the portion of a given SystemC HLS design’s simulation behavior that is related to the erroneous output(s). Experimental results including an extensive set of standard SystemC HLS designs show the effectiveness of our approach in localizing the designs’ simulation behavior in terms of the number of visualized variables. In comparison to traditional visualization methods, our proposed approach obtains up to 96% and 91% reduction in the search space for single and multiple faulty outputs, respectively.

Quantum computers offer enormous speed advantages over their classical counterparts. Still, optimization on quantum circuits is necessary to further increase their potential. Additionally, physical realizations of quantum computers place restrictions on quantum circuits, regarding the available quantum gates. In order to satisfy these restrictions, non-native gates need to be expressed as an equivalent cascade of natively available quantum gates which induces a mapping overhead. Two complementary approaches to this problem are to move around the qubits (using SWAP gates) or to apply so-called remote gates, i.e. pre-computed cascades of native gates which keep the qubit placement.In this paper, we explore how combinations of movements and remote gates can be employed to reduce the required overhead regarding the number of native gates as well as the circuit depth. We also discuss ways to find out which qubits to address with the movements in order to optimize these metrics. Our general evaluation is supplemented by evaluations on two IBM quantum computer architectures to show how quantum circuits can be optimized by the presented patterns.

Recently, Virtual Prototypes (VPs) implemented in SystemC TLM (Transaction-Level Modeling) have been introduced into the growing RISC-V ecosystem to facilitate early software development and testing. However, accurate environment modeling, which is crucial for Cyber-Physical Systems (CPS), has been mostly neglected to this point. Thus, in this paper, we propose the RISC-V AMS VP framework, that combines an existing open source RISC-V VP with the SystemC AMS (Analog/Mixed Signal) environment modeling style to obtain a RISC-V evaluation platform tailored for CPS. As a case study we created a temperature control system that integrates a sensor and heater component together with a control software. Moreover, we present results on an exemplary fault-injection evaluation that is enabled by bringing together software, hardware and environment models in our unified RISC-V AMS VP framework. Finally, we provide the RISC-V AMS VP framework together with the temperature control system as open source to stimulate further research and as foundation for educational purposes.

The emergence of Virtual Prototypes (VPs) at the Electronic System Level (ESL) has played a major role in modernizing the System-on-Chips (SoCs) design flow to raise design productivity and reduce time-to-market constraint. Leveraging VPs and extending their use-cases for early security validation are shown as a promising direction. As the cost of fixing any security flaws increases with the stage of development, VP-based security validation can significantly avoid costly iterations. In this paper, we propose VIP-VP, a novel VP-based dynamic information flow analysis approach at the ESL.VIP-VP enables designers to validate the information flow policies of a given VP-based SoC against security threat models, such as information leakage (confidentiality) and unauthorized access to data in a memory (integrity). Experimental results including a real-world VP-based SoC demonstrate the scalability and applicability of the proposed approach.

Constrained IoT devices with limited computing resources are on the rise. They utilize low-end multithreaded operating systems (e.g. RIOT) where each thread is assigned a fixed stack size during the development process. In this regard, it is important to choose an appropriate stack size which does not cause stack overflows and at the same time does not waste scarce memory resources by overestimating the required thread stack size. In this paper we propose an in-vivo technique for stack overflow detection and stack size estimation that leverages Virtual Prototypes (VPs) and is specifically tailored for low-end multithreaded IoT operating systems. We focus on SystemC-based VPs which operate on the TLM abstraction level. VPs are an industrial proven modeling standard to enable early software development and testing. We propose a non-intrusive extension for existing VPs which allows detecting stack overflows and provides a stack size estimation, which is beneficial to a VP-based development process. Our analysis works in-vivo, hence no modification of the executed software binary is required between testing and deployment. Our evaluation using the RIOT operating system revealed two previously unknown stack overflows in RIOT and identified potential stack size overestimation.

We present a tool that allows developers to debug hard- and software and their interaction in an early design stage. We combine a SystemC virtual prototype (VP) with an easily configurable and interactive graphical user interface and a standard software debugger. The graphical user interface visualizes the internal state of the hardware. At the same time, the software debugger monitors and allows to manipulate the state of the software. This co-visualization supports design understanding and live debugging of the HW/SW interaction. We demonstrate its usefulness with a case-study where we debug an OLED display driver running on a RISC-V VP.

Modern System-on-Chips (SoCs) have been increasingly deployed in critical aspects of our lives. As a consequence, they have access to a large number of secret assets that must be protected against unauthorized access. In order to provide sound security guarantees, an SoC typically has a security architecture as authentication mechanisms to control the access of different Intellectual Properties (IPs) to secret assets. Since the SoC's security architecture cannot be changed after production, it is of utmost importance to detect any security flaws in the design phase. Moreover, to prevent costly fixes in later stages, security validation should start as early as possible. In this paper, we propose a novel approach to validate the security architecture of a given SoC against timing flows using SystemC-based Virtual Prototype (VP) and static information flow tracking technique at the system level. Experimental results on two real-world VP-based SoCs demonstrate the scalability and applicability of the proposed approach in identifying timing flows.

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.

Verifying the functional correctness of a circuit is often the most time-consuming part of the design process. Recently, world-level formal verification methods, e.g., Binary Moment Diagram (BMD) and Symbolic Computer Algebra (SCA) have reported very good results for proving the correctness of arithmetic circuits. However, these techniques still frequently fail due to memory or time requirements. The unknown complexity bounds of these techniques make it impossible to predict before invoking the verification tool whether it will successfully terminate or run for an indefinite amount of time.

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.

In this work, we sketch an automated design flow for hardware synthesis based on a formal specification. Verification results are propagated from the FSL level through the proposed flow to generate an ESL model as well as an RTL implementation automatically. In contrast, the established design flow relies on manual implementations at the ESL and RTL level. The proposed design flow combines proof assistants with functional hardware description languages. This combination decreases the implementation effort significantly and the generation of test benches is no longer needed. We illustrate our design flow by specifying and synthesizing a set of benchmarks that contain sequential and combinational hardware designs. We compare them with implementations required by the established hardware design flow.

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.

The design of modern systems has reached a complexity which makes it inevitable to apply verification methods in order to guarantee its correct and safe execution. The verification methods frequently produce proof obligations that can not be solved any more due to the huge search space. However, by setting enough variables to fixed values, the search space is obviously reduced and solving engines eventually may be able to complete the verification task. Although this results in a partial verification, the results may still be valuable — in particular as opposed to the alternative of no verification at all. However, so far no systematic investigation has been conducted on which variables to fix in order to reduce verification runtime as much as possible while, at the same time, still getting most coverage. This paper addresses this question by proposing a corresponding verification runtime analysis. Experimental evaluations confirm the potential of this approach.

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.

The massive increase in computation power leads to a renaissance of supervised learning techniques, which were published decades ago but have so far been confined to theory. These techniques form the increasingly important field of Machine Learning (ML), which contributes to a large variety of research concerning industrial, automotive but also consumer applications strongly influencing our daily life. Commonly, the learning techniques require a set of labeled data, which involves a resource-intensive generation, to conduct the training. Depending on the dimensionality of the data and the required precision as needed by the application, the amount of training data varies. In case of insufficient training data, the prediction is of low-quality or not even possible at all, restricting the applicability of ML. This work proposes a combination of formal techniques and ML to implement a framework that allows coping with high-dimensional, training data while retaining a high prediction quality. The efficacy of this method is exemplarily demonstrated on the basis of an interdisciplinary material science research problem concerning the development of new structural materials, though it can be adapted to further applications.

Field-coupled Nanocomputing (FCN) is a computing concept with several promising post-CMOS candidate implementations that offer tremendously low power dissipation and highest processing performance at the same time. Two of the manifold physical implementations are Quantum-dot Cellular Automata (QCA) and Nanomagnet Logic (NML). Both inherently come with domain-specific properties and design constraints that render established conventional design algorithms inapplicable. Accordingly, dedicated design tools for those technologies are required. This paper provides an overview of two leading examples of such tools, namely fiction and ToPoliNano. Both tools provide effective methods that cover aspects such as placement, routing, clocking, design rule checking, verification, and logical as well as physical simulation. By this, both freely available tools provide platforms for future research in the FCN domain.

With more and more powerful quantum computers becoming available, there is an increasing interest in the efficient mapping of a given quantum circuit to a particular quantum computer (so-called technology mapping). In most cases, the limitations of the targeted quantum hardware have not been taken into account when generating these quantum circuits in the first place. Thus, the technology mapping is likely to induce a considerable overhead for such circuits. In this paper, we consider the realization of reversible circuits consisting of multiple-controlled Toffoli gates on IBM quantum computers. We show that choosing different quantum-level decompositions can indeed have a significant impact on the mapping overhead. Based on this observation, we present an approach to perform design space exploration to obtain quantum circuits with reduced overhead by exploiting information about the targeted quantum hardware as well as the reversible circuit. An experimental evaluation shows that this approach often leads to considerable reductions of the technology mapping overhead with negligible runtime.

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.

In order to meet time-to-market constraints and to raise the design productivity, High-level Synthesis (HLS) is being increasingly adopted by the semiconductor industry. HLS designs, which can be automatically translated into Register Transfer Level (RTL), are typically written in SystemC at the Electronic System Level (ESL). However, this modern design flow still has weaknesses, in particular, due to the significant manual effort involved for verification and the subsequent debugging process which are both time-consuming and error-prone. In this paper, we propose ASCHyRO, a fully automated semiformal fault localization approach for SystemC HLS designs. ASCHyRO takes advantage of a hybrid rank ordering technique to derive a reduced ordered set of potential fault locations. The reduced order set is obtained by calculating a Confidence Score (CS) for each fault candidate based on a combination of static and dynamic fault probability analysis. Experimental results including an extensive set of standard SystemC HLS designs show the effectiveness of our approach in localizing even multiple faults with high confidence in a short execution time.

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.

Resistive random access memory (RRAM) is a nonvolatile memory technology which allows to perform computations in both digital and analog circuits. Multiply-Accumulate (MAC) is an analog column-based operation enabled on RRAM crossbars providing high efficiency to perform complex matrix vector multiplications, which is attractive for neural network accelerators. However, the analog computational capability of RRAM devices has not been yet utilized for logic synthesis. In this paper, we show how a synthesis approach based on binary decision diagrams (BDD) can efficiently exploit efficient MAC computation enabled by RRAM. The proposed approach highly benefits from a symmetric structure of Boolean functions. Therefore, a design methodology is presented which optimizes and approximates BDDs under provided error thresholds to maximize efficiency of synthesized logic circuits under negligible loss of accuracy. In the experiments, we show that our proposed synthesis approach allows for an average reduction of up to 47% in the number of operations and up to 66% in the number of required devices compared to state-of-the art methods, even without approximation. Using approximation, we can further reduce the number of required devices.

In computer programming education, learning to program tangible objects has become a common way to introduce programming to young students. In an effort to address this intervention, scientific research has been done on the effectiveness of using tangible hardware platforms such as robots and wearable products to teach basic programming concepts to children. However, there is a lack of research on how young students' attitudes and programming skills are influenced over time, when they learn to program tangible objects and make them smart. In this paper, we investigate the impacts of using a tangible everyday object and making it smart on young female students' attitudes towards programming and the acquisition of basic programming skills. During a 4-day non-formal programming workshop with 12 6th grade students, they were introduced to basic programming concepts, and learned how to apply them to turn a houseplant into a smart object. In a pilot study, we employed a block-based programming environment and analyzed the students' trajectories of attitudes towards programming and performance based on repeated open-ended qualitative questionnaires and programming questions throughout the workshop. The results show that all students had high confidence regarding programming skills, regardless of creating smart objects. Furthermore, it indicates that experienced students highly valued the programming of tangible everyday objects compared with inexperienced students. The findings of this work contribute to our understanding of how making tangible everyday objects smart can support the development of a positive attitude and keep up of interest throughout a programming workshop among girls.

Near zero-energy computing describes the concept of executing logic operations below the ( k B T ln 2) energy limit. Landauer discussed that it is impossible to break this limit as long as the computations are performed in the conventional, non-reversible way. But even if reversible computations were performed, the basic energy needed for operating circuits realized in conventional technologies is still far above the ( k B T ln 2) energy limit (i.e., the circuits do not operate in a physically reversible manner). In contrast, novel nanotechnologies like Quantum-dot Cellular Automata (QCA) allow for computations with very low energy dissipation and hence are promising candidates for breaking this limit. Accordingly, the design of reversible QCA circuits is an active field of research. But whether QCA in general and the proposed circuits in particular are indeed able to operate in a logically and physically reversible fashion is unknown thus far, because neither physical realizations nor appropriate simulation approaches are available. In this work, we address this gap by utilizing an established theoretical model that has been implemented in a physics simulator enabling a precise consideration of how energy is dissipated in QCA designs. Our results provide strong evidence that QCA is indeed a suitable technology for near zero-energy computing. Further, the first design of a logically and physically reversible adder circuit is presented, which serves as proof of concept for future circuits with the ability of near zero-energy computing.

Due to the ever increasing complexity of hardware systems, designers strive for higher levels of abstractions in the early stages of the design process. Modeling hardware at the electronic system level (ESL) is one way to address this demand, with the C++-based system modeling framework SystemC and its abstract communication library transaction level modeling (TLM) having become de-facto standards for ESL system design. While the C++ compiler is sufficient to compile and simulate a given ESL design, for tasks of design understanding, debugging, or validation (where access to the details of design's structure and behavior is necessarily required), design needs to be processed by an appropriate tool. This problem is often solved by adding instrumentation code to either the design or the library, usually resulting in incomplete logs, work overhead and/or incompatibilities. This paper introduces an approach that automatically extracts information about both, structure and behavior of SystemC designs and TLM transactions, nonintrusively. The information is retrieved from a given design by running it in debug mode while being connected to a preprogrammed debugger, thus leaving the existing sources and workflows untouched while collecting a vast amount of data without user intervention. Illustrating use cases, value change dump files of the SystemC models' behavior and unified modeling language activity diagrams of transaction protocols are created automatically from simulation runs.

Quantum computation promises to solve many hard or infeasible problems substantially faster than classical solutions. The involvement of big players like Google, IBM, Intel, Rigetti, or Microsoft furthermore led to a momentum which increases the demand for automated design methods for quantum computations. In this context, decision diagrams for quantum computation provide a major pillar as they allow to efficiently represent quantum states and quantum operations which, otherwise, have to be described in terms of exponentially large state vectors and unitary matrices. However, current decision diagrams for the quantum domain suffer from a tradeoff between accuracy and compactness, since: 1) small errors that are inevitably introduced by the limited precision of floating-point arithmetic can harm the compactness (i.e., the size of the decision diagram) significantly and 2) overcompensating these errors (to increase compactness) may lead to an information loss and introduces numerical instabilities. In this article, we describe and evaluate the effects of this tradeoff which clearly motivates the need for a solution that is perfectly accurate and compact at the same time. More precisely, we show that the tradeoff indeed weakens current design automation approaches for quantum computation (possibly leading to corrupted results or infeasible run-times). To overcome this, we propose an alternative approach that utilizes an algebraic representation of the occurring complex and irrational numbers and outline how this can be incorporated in a decision diagram which is suited for quantum computation. Evaluations show that-at the cost of an overhead which is moderate in many cases-the proposed algebraic solution indeed overcomes the tradeoff between accuracy and compactness that is present in current numerical solutions.

The increasing functionality of electronic systems due to the constant evolution of the market requirements makes the non-functional aspects of such systems (e.g., energy consumption, area overhead, or performance) a major concern in the design process. Approximate computing is a promising way to optimize these criteria by trading accuracy within acceptable limits. Since the cost of applying significant structural changes to a given design increases with the stage of development, the optimization solution needs to be incorporated into the design as early as possible. For the early design entry, modeling hardware at the Electronic System Level (ESL) using the SystemC language is nowadays widely used in the industry. To apply approximation techniques to optimize a given SystemC design, designers need to know which parts of the design can be approximated. However, identifying these parts is a crucial and non-trivial starting point of approximate computing, as the incorrect detection of even one critical part as resilient may result in an unacceptable output. This usually requires a significant programming effort by designers, especially when exploring the design space manually. In this article, we present PREASC, a fully automated framework to identify the resilience portions of a given SystemC design. PREASC is based on a combination of static and dynamic analysis methods along with regression analysis techniques (a fast machine learning method providing an accurate function estimation). Once the resilient portions are identified, an approximation degree analysis is performed to determine the maximum error rate that each resilient portion can tolerate. Subsequently, the maximum number of resilient portions that can be approximated at the same time are reported to designers at different granularity levels. The effectiveness of our approach is evaluated using several standard SystemC benchmarks from various domains.

In light of the complexity of introductory programming for young learners, visual programming has become more and more popular. In particular, block-based educational programming systems have emerged as an area of active research. This paper introduces an educational block-based programming application, enabling young learners to learn and make programs in the context of smart homes. In this application, smart objects have a set of primitive behaviors which can be integrated in the general features of programming languages like variables, conditionals, loops, and functions. The programming language is shown in a graphical interface to enable young students to program with the application. The development and implementation of this application, along with helping features for the students are described. In a pilot study with 20 7th grade students, the application's effectiveness and ease of use are evaluated. The results show that students can fairly solve programming problems and make real programs in the context of smart homes. Feedback of the learners is presented and discussed.

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.

This paper introduces a new method to trace cycle-accurately the temporal behavior of on-chip signals while operating in-field. Current cycle-accurate schemes incur unacceptable amounts of data for logging, storage and processing.

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.

This paper investigates the benefits of verifying embedded systems after deployment. We argue that one reason for the huge state spaces of contemporary embedded and cyber-physical systems is the large variety of operating contexts, which are unknown during design. Once the system is deployed, these contexts become observable, confining several variables. By this, the search space is dramatically reduced, making verification possible even on the limited resources of a deployed system. In this paper, we propose a design and verification flow which exploits this observation. We show how specifications are transferred to the deployed system and verified there. Evaluations on a number of case studies demonstrate the reduction of the search space, and we sketch how the proposed approach can be employed in practice.

Quantum computation is a promising research field since it allows to conduct certain tasks exponentially faster than on conventional machines. As in the conventional domain, decision diagrams are heavily used in different design tasks for quantum computation like synthesis, verification, or simulation. However, unlike decision diagrams for the conventional domain, decision diagrams for quantum computation as of now suffer from a trade-off between accuracy and compactness that requires parameter fine-tuning on a case-by-case basis. In this work, we-for the first time-describe and evaluate the effects of this trade-off. Moreover, we propose an alternative approach that utilizes an algebraic representation of the occurring irrational numbers and outline how this can be incorporated in a decision diagram in order to overcome this trade-off.

Computers are involved in our every-day life, making increasingly consequential decisions. This raises the question of the ethics of these decisions, for example when autonomous cars are concerned. We argue that the ethics of the decisions taken by a computer are in fact those of the developers, encoded in the program ("code is ethics"). This encoding is mostly implicit - programmers and users are often even not aware of the implicit decisions that are being made before the program is even run. We suggest that formal methods are an excellent way to make the criteria under which these decisions are taken explicit, because formal specifications are more concise, abstract and clearer than code, This way, it becomes clear why systems act the way they do, and where the responsibility for their behaviour lies.

Virtual Prototypes (VPs) at the Electronic System Level (ESL) written in SystemC language using its Transaction Level Modeling (TLM) framework are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models implemented at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for an early design verification. Hence, the correctness assurance of these reference models (VPs) is critical as undetected faults may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we propose a novel simulation-based verification approach to automatically validate the simulation behavior of a given SystemC VP against both the TLM-2.0 rules and its specifications (i.e. functional and timing behavior of communications in the VP). The scalability and the efficiency of the proposed approach are demonstrated using an extensive set of experiments including a real-word VP.

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.

This work presents a novel hybrid compression architecture that seamlessly combines the advantages of an embedded test compression technique with a lightweight codeword-based compression scheme. The proposed architecture tackles the shortcomings of state-of-the-art techniques, which are widely to address the rising challenges of safety-critical applications enforcing a zero defect policy. Embedded test compression techniques had been introduced that allow the compression of a large share of the test patterns. However, depending on the test application (e.g. low pin count test) there is a certain number of test patterns, which are incompressible due to the architecture and will be rejected. This leads to a test coverage decrease which, in turn, jeopardizes the zero defect policy. Therefore, the rejected test patterns are typically transferred in an uncompressed way bypassing the embedded compression, which is extremely costly. The proposed hybrid architecture mitigates the adverse impact of rejected test patterns on the compression ratio as well as on the test application time of state-of-the-art techniques. The experimental evaluation of industrial-sized designs clearly shows that a significant compression ratio up to 67.4 % and a test application time reduction up to 65.7% can be achieved.

With the increase in circuit complexity, the gap between circuit development time and analysis time has widened. A large database is required in order to perform essential analysis tasks such as power, thermal, and IR-drop analysis, which, in turn, leads to long run times. This work focuses on test power analysis. Due to the large number of test patterns for modern designs and the excessive power analysis run time for each test, it is not feasible to obtain complete power profiles for all the tests. However, test power-safety is essential to produce reliable manufacturing test results and prevent yield loss and chip damage. Accurate power profiling can typically be done for a small subset of pre-selected tests only. An essential task is therefore to determine those tests, which potentially provide the worst-case scenarios with respect to test power. We propose machine learning-based power prediction for test selection. The prediction is applied in two different ways. First, we predict the activity of a test to identify tests with high power consumption. Second, the switching activity and the power information are related to the layout of the chip to identify local hot spots. Various machine learning-based algorithms are used to evaluate this approach. Additionally, the algorithms are compared against each other. The results indicate high prediction accuracy and effectiveness. This makes these algorithms well suited for worst-case test selection.

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.

Safety and dependability are of utmost importance for many integrated systems. Hence, it must be guaranteed throughout the whole system's lifetime that no ambient and internal influences can affect the system's integrity. Under this scope and having in mind the side-effects of today's nanoscale technologies, hardware degradation is of rising concern. However, related studies should not solely focus on aging effect itself, but also consider its relation to any accelerating factors, especially temperature. Towards this end, this work presents a study on how the power dissipation of a circuit, and thus, its temperature, can expedite wear-out effects. Therefore, three different analysis are performed-aging without and with consideration of temperature and the study on how guard-banding strategies are affected. In order to distinguish random and, maliciously intended or accidentally produced, worst case scenarios, we implemented an algorithm that determines a combination of input vectors that forces high aging states and high power dissipation. Results indicate that aging under consideration of temperature can increase circuit delay by more than 26% (random case) and by nearly 40% (worst case). That means, if a maximum acceptable delay degradation is defined, designs can enter malfunction states already in a period of weeks (worst case) or months (random case). These results underline the importance of considering power dissipation, and thus temperature, when doing aging analysis and aging verification.

This work presents a novel hybrid compression architecture that seamlessly combines the advantages of an embedded test compression technique with a lightweight codeword-based compression scheme. Embedded test compression has proven to be beneficial and is widely used in industrial circuit designs. However, particularly, in test applications within low-pin-count environments, a certain number of test patterns is incompressible and will, therefore, be rejected. This leads to a test coverage decrease which, in turn, jeopardizes the zero defect policy of safety-critical applications like automotive microcontrollers. Therefore, the rejected test patterns are typically transferred in an uncompressed way bypassing the embedded compression, which is extremely costly. The proposed hybrid architecture mitigates the adverse impact of rejected test patterns on the compression ratio as well as on the test application time of state-of-the-art techniques. The experimental evaluation of industrial-sized designs clearly shows that a significant compression ratio up to 67.4% and a test application time reduction up to 72.9% can be achieved when utilizing the existing multi-channel interfaces.

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.

I. VLSI Systems: A Glance Into The Last Decades Since their inception in 1970s, VLSI systems have enabled several new technological capabilities and made them accessible to an unceasingly wider range of users, reaching a scale that has been exponentially increasing over the decades[1](seeFig. 1). Relentless integration of more complex systems has driven such remarkable evolution, as made possible by the inexorable miniaturization. As shown inFig. 1, more functionality has been crammed in a consistently smaller form factor, as exemplified by the physical volume shrinking of computers by 100 X/decade[2],[3]. At the same time, the energy per task has been decreasing at 10–100 X/decade, as shown inFig. 2, for several systems and system-on-chip subsystems[4]. This allowed packing more capabilities into the same power envelope, as generally observed in the electronic systems, even before the advent of the integrated circuit[5].

Due to their shrinking feature sizes as well as environmental influences, such as high-energy radiation, electrical noise, and particle strikes, integrated circuits are getting more vulnerable to transient faults. Accordingly, how to make those circuits more robust has become an essential step in today's design flows. Methods increasing the robustness of circuits against these faults already exist for a long period of time but either introduce huge additional logic, change the timing behavior of the circuit, or are applicable for dedicated circuits such as microprocessors only. In this paper, we propose an alternative method, which overcomes these drawbacks by determining application-specific knowledge of the circuit, namely the relations of flip-flops and when they assume the same value. By this, we exploit partial redundancies, which are inherent in most circuits anyway (even the optimized ones), to frequently compare the circuit signals for their correctness-eventually leading to an increased robustness. Since determining the correspondingly needed information is a computationally hard task, formal methods, such as bounded model checking, satisfiability-based automatic test pattern generation, and binary decision diagrams, are utilized for this purpose. The resulting methodology requires only a slight increase in additional hardware, does only influence the timing behavior of the circuit negligibly, and is automatically applicable to arbitrary circuits. Experimental evaluations confirm these benefits.

Reversible circuits employ a computing paradigm that is useful in a broad variety of applications. With increasing interest, security concerns for those circuits also will rise in the near future. At first glance, reversible circuits seem to be more secure to integrated circuit (IC)/intellectual property (IP) piracy than conventional circuits, since the target function is usually embedded in the reversible backbone circuit. This embedding adds ancillary inputs and garbage outputs that may appear to hide the target function. However, recent work showed that target function embedding and reversible synthesis methods leave telltale signs in the reversible circuits, which allow for an easy extraction of the synthesis approach and the embedded circuit. In this article, we perform an analysis of the IC/IP piracy attacks on reversible circuits. We focus on the reversible circuits generated by the quantum multivalued decision diagram (QMDD)- and binary decision diagram (BDD)-based synthesis approaches as case studies. We show that most of the target function can be identified using the telltale signs of the synthesis approach. We then propose a cost-effective input-output scrambling scheme that wipes out these telltale signs and, thus, thwarts the considered attacks by adding reversible gates. Those additional gates yield efficient yet secure reversible circuits.

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.

The Clifford+T library provides robust and fault-tolerant realizations for quantum computations. Consequently, (logic) synthesis of Clifford+T quantum circuits became an important research problem. However, previously proposed solutions are either only applicable to very small quantum systems or lead to circuits that are far from being optimal- mainly caused by a local, i.e. column-wise, consideration of the underlying transformation matrix to be synthesized. In this paper, we suggest an improved approach that considers the matrix globally and, by this, overcomes many of these drawbacks. Preliminary evaluations show the promises of this direction.

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.

Highly compact as well as compressed test pattern generation may result in the aggregation of high power activity in specific areas on a manufactured circuit during testing. These hotspots can lead to electromigration and IR-drop in local blocks of the chip resulting in wrong test results. This is due to the circumstance that the effect of localized high switching activity is not precisely taken into consideration during ATPG and pattern simulation. Discarding such patterns may result in test coverage loss. Low power test generation methods typically reduce the switching activity globally across the pattern and not locally in specific areas. Additionally, these methods typically increase the test data volume as well as the testing time. In this paper, a test pattern retargeting methodology is proposed which takes pattern- specific, dynamically identified hotspots into account. Critical patterns and their corresponding critical regions are identified. Based on this data, constraints are used for pattern retargeting preventing the previously identified local hotspots. In contrast to previous methods, the proposed retargeting technique ensures a high test coverage without a large pattern inflation.

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) is a field-coupled nanotechnology which might enable design with high performance and extraordinary low energy dissipation. Infor-mation processing and flow in QCA is controlled by external clocks, which requires a proper synchronization already during circuit design phase. In this paper, we discuss the fundamental differences between local and global synchronicity in QCA circuits. Further, we show that it is possible to relax the global synchronicity constraint and discuss the consequent impact on the design performance. Simulation results indicate that the design size can be reduced by about 70% while the throughput performance declines by similar values.

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.

This overview paper summarizes the content of a tutorial given at the 2018 edition of the Forum on specification & Design Languages. The aim of the tutorial was to introduce the technology of microfluidic devices, which gained significant interest in the recent past, as well as corresponding design challenges to a community focused on design automation and corresponding specification/design languages. By this, the overview presents a starting point for researchers and engineers interested in getting involved in this area.

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.

Reversible logic is a building block for adiabatic and quantum computing in addition to other applications. Since common functions are non-reversible, one needs to embed them into proper-size reversible functions by adding ancillary inputs and garbage outputs. We explore the Intellectual Property (IP) piracy of reversible circuits. The number of embeddings of regular functions in a reversible function and the percent of leaked ancillary inputs measure the difficulty of recovering the embedded function. To illustrate the key concepts, we study reversible logic circuits designed using reversible logic synthesis tools based on Binary Decision Diagrams and Quantum Multi-valued Decision Diagrams.

The probability that a particular device is operational for a given duration, or reliability, is a dependability attribute and key metric for systems in critical applications. For example, systems for long-term autonomous exploration missions have to be operational during their complete mission. Other critical applications like banking, medical automotive or aerospace face similar reliability requirements that are only met by dependable systems. Traditional dependable systems, compared to their non-dependable counterparts, have three key issues: They are more expensive, consume more power, and provide less performance.

As digital circuits have become more complicated than ever, abstract description languages such as SystemC have been introduced, allowing designers to work on more abstract levels during the design process. Design metrics such as performance and energy consumption are a central concern for designers at all levels of abstraction. Approximate computing is a promising way to optimize these criteria, sacrificing accuracy. Defining which parts of a design can be approximated (and to what degree) is a crucial and non-trivial design decision, which is usually connected to a larger programming effort, especially when exploring the design space manually. In this paper, we propose an automated approach based on machine learning techniques in order to detect the resilience of a given SystemC design's modules. This is used to identify components of the design that can be approximated. The effectiveness of the proposed method is evaluated using several SystemC benchmarks from various domains.

Design of nonvolatile in-memory computing devices has attracted high attention to resistive random access memories (RRAMs). We present a comprehensive approach for the synthesis of resistive in-memory computing circuits using binary decision diagrams, and-inverter graphs, and the recently proposed majority-inverter graphs for logic representation and manipulation. The proposed approach allows to perform parallel computing on a multirow crossbar architecture for the logic representations of the given Boolean functions throughout a level-by-level implementation methodology. It also provides alternative implementations utilizing two different logic operations for each representation, and optimizes them with respect to the number of RRAM devices and operations, addressing area, and delay, respectively. Experiments show that upper bounds of the aforementioned cost metrics for the implementations obtained by our synthesis approach are considerably improved in comparison with the corresponding existing methods in both area and especially latency.

Quantum-dot cellular automata (QCA) are an emerging field-coupled nanotechnology with remarkable performance and energy efficiency. In order to enable the exploration of this technology, we propose a model for the logic synthesis of QCA circuits that, for the first time, considers and abstracts all main physical aspects-in particular, energy dissipation. To this end, we review in detail how energy is dissipated in QCA cells and present a corresponding environment that allows for the estimation of the energy dissipation with respect to any specific set of technology parameters. Based on that, we derive a model for logic synthesis. A case study confirms the accuracy of the proposed model and reveals that interconnections have a significant impact in this technology-motivating a more rigorous consideration. These findings eventually provide the basis for a new generation of synthesis approaches at the logic level that are explicitly dedicated to QCA systems.

Due to shrinking feature sizes, integrated circuits are getting more vulnerable against transient faults. Methods increasing the robustness of circuits against these faults already exist for a long period of time but either introduce huge additional logic, increase the latency of the circuit, or are applicable for dedicated circuits such as microprocessors only. This work proposes an alternative hardening method which requires only a slight increase in additional hardware, does not influence the timing behavior, and is automatically applicable to arbitrary circuits. To this end, application-specific knowledge of the considered circuit is exploited, analyzed by a dedicated orchestration of formal techniques, and, eventually, used to synthesize a fault detection mechanism enhancing the robustness of the circuit. Experimental evaluations show that the proposed solution leads to a significant increase in the robustness, while the hardware overhead is kept moderate.

Digital microfluidics is an emerging technology that provide fluidic-handling capabilities on a chip. One of the most important issues to be considered when conducting experiments on the corresponding biochips is the routing of droplets. A recent variant of biochips uses a micro-electrode-dot-array (MEDA) which yields a finer controllability of the droplets. Although this new technology allows for more advanced routing possibilities, it also poses new challenges to corresponding CAD methods. In contrast to conventional microfluidic biochips, droplets on MEDA biochips may move diagonally on the grid and are not bound to have the same shape during the entire experiment. In this work, we present an exact routing method that copes with these challenges while, at the same time, guarantees to find the minimal solution with respect to completion time. For the first time, this allows for evaluating the benefits of MEDA biochips compared to their conventional counterparts as well as a quality assessment of previously proposed routing methods in this domain.

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.

With the increase in transistor density in state-of-the-art circuits the power behavior of integrated circuits changes drastically, which may result in device failures. This may become worse while testing, because of the high transient activity in smaller area. This may lead to high power consumption and failures in certain areas as compared to other parts of the die. For this reason, high power density areas on the integrated circuits need to be identified on the layout to avoid effects such as IR-drop, EM and noise as early as possible. Previously, this was usually considered by manually dividing the layout in equal blocks. However, this method may not provide the desired accuracy due to e.g. boundary effects and manual errors. In this paper, we propose the use of pattern recognition/machine learning techniques to dynamically partition the layout in clusters to identify high power density areas under test application. We show how machine learning techniques can be used to model the clustering problem and analyze the feasibility as well as the performance of several algorithms on benchmark circuits. These techniques avoid the errors on static boundaries and account for pattern dependent behavior. Furthermore, the proposed clustering is validated by comparing the results to a contour of an industrial tool.

The necessity to handle the increasing complexity of digital circuits has led to the usage of more and more abstract design paradigms. In particular, the Electronic System Level (ESL) has become an area of active research and industrial application, especially via SystemC and its Transaction Level Modeling (TLM) framework. Additionally, the usage of formal specification languages such as the Unified Modeling Language (UML) prior to the implementation (even at higher abstraction levels) is now a broadly accepted workflow. Utilizing this layered approach leaves the translation from the specification to the implementation to the designer, leaving the question unanswered how the equivalence of these should be verified. This paper proposes a novel, non-intrusive and broadly applicable approach to automatically validate the equivalence of the structural and behavioral information of a SystemC-TLM 2.0 model and its formal specification.

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.

We present a formal optimization technique that enables retargeting for codeword-based IEEE 1149.1-compliant TAP controllers. The proposed method addresses the problem of high test data volume and Test Application Time (TAT) for a system-on-chip design during board or in-field testing, as well as during debugging. This procedure determines an optimal set of codewords with respect to given hardware constraints, e.g., embedded dictionary size and the interface to the Test Data Register in the IEEe 1149.1 Std. A complete traversal of the spanned search space is possible through the use of formal methods. An optimal set of codewords can be determined, which is directly utilized for retargeting. The proposed method is evaluated using test data with high-entropy, which is known to be the least amenable to compression, as well as input data for debugging and Functional Verification (FV) test data. Our results show a compression ratio improvement of more than 30% and a reduction in TAT up to 20% compared to previous techniques.

Digital Microfluidic Biochips (DMFBs) are an emerging technology promising a high degree of automation in laboratory procedures by means of manipulating small discretized amounts of fluids. A crucial part in conducting experiments on biochips is the routing of discretized droplets. While doing so, droplets must not enter each others' interference region to avoid unintended mixing. This leads to cells in the proximity of the droplet being impassable for others. For different cell shapes, the effect of these temporary blockages varies as the adjacency of cells changes with their shapes. Yet, no evaluation with respect to routability in relation to cell shapes has been conducted so far. This paper analyses and compares various tessellations for the field of cells. Routing benchmarks are mapped to these and the results are compared in order to determine if and how cell shapes affect the performance of DMFBs, showing that certain cell shapes are superior to others.

Resistive Random Access Memory (RRAM) is a promising non-volatile memory technology which enables modern in-memory computing architectures. Although RRAMs are known to be superior to conventional memories in many aspects, they suffer from a low write endurance. In this paper, we focus on balancing memory write traffic as a solution to extend the lifetime of resistive crossbar architectures. As a case study, we monitor the write traffic in a Programmable Logic-in-Memory (PLiM) architecture, and propose an endurance management scheme for it. The proposed endurance-aware compilation is capable of handling different trade-offs between write balance, latency, and area of the resulting PLiM implementations. Experimental evaluations on a set of benchmarks including large arithmetic and control functions show that the standard deviation of writes can be reduced by 86.65% on average compared to a naive compiler, while the average number of instructions and RRAM devices also decreases by 36.45% and 13.67%, respectively.

On behalf of the Program, Organizing, and Steering Committees, we would like to extend a warm welcome to everyone attending the European Test Symposium 2017 (ETS'17). ETS has been established as one of the main international forums and the larger forum in Europe that brings together the test community to discuss emerging ideas, views, and trends in the area of electronic-based circuits and system testing. Topics of interest include, but are not limited to, design-for-test, dependability, security, failure analysis and diagnosis, on-line test, automated test hardware, validation and verification, fault simulation, fault tolerance, automatic test generation, etc.

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.

Optical circuits received significant interest as a promising alternative to existing electronic systems. Because of this, also the synthesis of optical circuits receives increasing attention. However, initial solutions for the synthesis of optical circuits either rely on manual design or rather straight-forward mappings from established data-structures such as BDDs, SoPs/ESoPs, etc. to the corresponding optical netlist. These approaches hardly utilize the full potential of the gate libraries available in this domain. In this paper, we propose an alternative synthesis solution based on AND-Inverter Graphs (AIGs) which is capable of utilizing this potential. That is, a scheme is presented which dedicatedly maps the given function representation to the desired circuit in a one-to-one fashion - yielding significantly smaller circuit sizes. Experimental evaluations confirm that the proposed solution generates optical circuits with up to 97% less number of gates as compared to existing synthesis approaches.

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.

The increasing complexity of todays digital circuit designs led to the increased usage of abstract models. In particular, the Electronic System Level (ESL) has emerged as an area of active research. For ESL design, SystemC and its Transaction Level Modeling (TLM) framework have become the standard tools for abstract modeling. The resulting models represent both, an executable specification and a reference model for the hardware design. The correctness of these designs is important as undetected errors may propagate to less abstract levels in the design process, increasing the potential amount of work required to fix them. To quickly ensure that implementations and reference emit the same behavior, the comparison between these abstractions needs to be both, flexible and automated. This paper presents a method to verify the simulation behavior of a given System TLM-2.0 design against TLM-2.0 protocols. The system's structural description and its run-time behavior are translated to a single, consistent formal model. This is then used to verify that a simulation run adheres to a given protocol. The protocol compliance checks are performed using the UPPAAL model checker and applied to several TLM models.

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.

UML/OCL models are used to describe system models in early stages of the design process. In order to detect design flaws in these models as soon as possible (ideally before the implementation phase starts), various methods for the validation and verification of UML/OCL models have been proposed. In particular, automatic solutions (so-called model finders) are of interest here. They provide designers with quick feedback, e. g., on the consistency of their models in a push-button fashion. But thus far, all proposed approaches support a (small) subset of UML/OCL only or employ substantial restrictions. In fact, there are only few solutions that support the extended type system including the irregular values null and invalid - although these values play an important role for covering exceptional cases. Moreover, these solutions either heavily rely on manual interaction or significantly restrict the supported UML/OCL description means. In this work, we propose a generic formal representation of UML/OCL which can be used for the validation and verification of corresponding models and, at the same time, addresses these shortcomings.

The use of formal models to describe early versions of the structure and the behavior of a system has become common practice in industry. UML and OCL are the de-facto specification languages for these tasks. They allow for capturing system properties and module behavior in an abstract but still formal fashion. At the same time, this enables designers to detect errors or inconsistencies in the initial phases of the design flow-even if the implementation has not already started. Corresponding tools for verification of formal models got established in the recent past. However, verification results are usually not reused in later design steps anymore. In fact, similar verification tasks are applied again, e.g., after the implementation has been completed. This is a waste of computational and human effort. In this paper, we address this problem by proposing a method which checks a given implementation of a system against its corresponding formal method. This allows for transferring verification results already obtained from the formal model to the implementation and, eventually, motivates a new design flow which addresses verification across abstraction levels. This paper describes the applied techniques as well as their orchestration. Afterwards, the applicability of the proposed methodology is demonstrated by means of examples as well as a case study from an industrial context.

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.

Ensuring nearest neighbor compliance of quantum circuits by inserting SWAP gates has heavily been considered in the past. Here, quantum gates are considered which work on non-adjacent qubits. SWAP gates are applied in order to “move” these qubits onto adjacent positions. However, a decision how exactly the SWAPs are “moved” has mainly been made without considering the effect a “movement” of qubits may have on the remaining circuit. In this work, we propose a methodology for nearest neighbor optimization which addresses this problem by means of a look-ahead scheme. To this end, two representative implementations are presented and discussed in detail. Experimental evaluations show that, in the best case, reductions in the number of SWAP gates of 56% (compared to the state-of-the-art methods) can be achieved following the proposed methodology.

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.

Resistive memories have gained high research attention for enabling design of in-memory computing circuits and systems. We propose for the first time an automatic compilation methodology suited to a recently proposed computer architecture solely based on resistive memory arrays. Our approach uses Majority-Inverter Graphs (MIGs) to manage the computational operations. In order to obtain a performance and resource efficient program, we employ optimization techniques both to the underlying MIG as well as to the compilation procedure itself. In addition, our proposed approach optimizes the program with respect to memory endurance constraints which is of particular importance for in-memory computing architectures.

Resistive switching property enables various promising applications such as design of non-volatile in-memory computing devices which has attracted high attention to Resistive Random Access Memories (RRAMs). In this work, we present a multi-objective BDD optimization approach for RRAM based logic circuit design. Dissimilar to classical BDD optimization, evaluating the cost metrics of the circuits in this case does not only depend on the number of BDD nodes but is more advanced. We have utilized a non-dominated sorting genetic algorithm for bi-objective BDD optimization with respect to the number of required RRAMs and computational steps addressing the area and delay of the resulting circuits, respectively. The algorithm also allows preference to one of the objectives if it is of higher significance. Experimental results show that the proposed multi-objective genetic algorithm achieves considerable reduction in both aforementioned criteria in comparison with an existing approach.

This work presents a new dynamically configurable compression architecture to be integrated directly into the test access mechanism of System-on-Chip (SoC) designs using IEEE 1149 compliant interfaces. The proposed technique reduces the test data volume without loosing the full legacy support, no extra IO pins are needed and the additional allocated hardware resources are negligible. Particularly, this technique is suitable for board as well as in-field testing, which both use typically a Test Access Mechanism (TAM) like IEEE 1149. Here, strong memory limitations exist on the test equipment, which restrict the testing or debugging capabilities for complex designs. Various benchmarks for random test data, representing highly pre-compressed test data, as well as fully-specified test data for selected industrial circuit designs were run and discussed to evaluate this new approach. These experiments clearly show a high test data volume reduction. Additionally, a noticeable reduction of the overall number of required test cycles are achieved for most of the test cases.

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.

Design processes are increasingly moving to more abstract description levels; no single formalism can handle the complexities of modern designs. However, keeping designs consistent across different abstraction levels, in particular in the presence of changes, has up to now been an arduous manual task. This paper presents a framework which provides a uniform, interconnected representation of the descriptions across the abstraction levels, starting from natural language requirement specifications over SysML design specifications down to executable SystemC models, allowing to track changes on all levels of abstraction, and ensuring consistency throughout the development process. The framework has been implemented in a tool, CHIMPANC, to show its viability. It assists the developer by highlighting inconsistencies and proof obligations across various descriptions levels in order to simplify the development process.

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.

While previous decades have witnessed impressive accomplishments in the design and realization of conventional computing devices, physical boundaries and cost restrictions led to an increasing interest in alternative technologies (often referred to as Beyond CMOS or More than Moore technologies). In addition, these accomplishments also triggered many “complementary” applications and led to technologies providing an additional value to the conventional logic (often referred to as More than Moore). This led to a variety of emerging technologies such as Quantum Computation, Optical Circuits, or Microfluidic Biochips out of which many are considered very promising and some even entered the market recently. This poses new challenges to researchers and engineers working in computer-aided design. In this tutorial paper, we provide an overview on the main concepts of selected emerging technologies as well as the resulting design methods. To this end, we review the respective technological background and introduce the correspondingly used circuit models. Based on that, we show how computer-aided design has to adapt the common design tasks and review recently proposed solutions.

In order to overcome the ever increasing complexity of digital circuits, system design at the Electronic System Level (ESL) has become an area of active research. SystemC provides designers with a readily-available ESL framework, allowing them to design mixed hardware/software systems using a standardized C++ library. The analysis of the resulting designs is crucial to e.g. apply additional validation steps or assist designers during the development process. Existing approaches focus on the extraction of static information, providing designers with models that describe the structure of their system but not its behavior. In this paper, we introduce the Automated Intra-cycle Behavioral Analysis tool, AIBA. AIBA utilizes the GNU debugger to execute a two-step analysis that retrieves behavioral and architectural information of ESL designs. The proposed method is completely non-intrusive, allowing both SystemC designs and the standard tool flow to be used without any modification. Case studies confirm the benefits of the 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.

The specification of non-functional requirements, e. g., on timing forms an essential part of modern system design. Modeling languages such as MARTE/CCSL provide dedicated description means enabling engineers to formally define the ticking of the clocks to be implemented in terms of clock constraints and the actually intended timing behavior in terms of instant relations. But thus far, instant relations have only been utilized in order to monitor the correct execution of the clock constraints. In this work, we propose a methodology which, for the first time, verifies clock constraints against the given instant relations. To this end, the timing behavior is represented in terms of an automaton followed by its verification through satisfiability solvers. A case study illustrates the application of the proposed methodology.

Verification and validation of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades - except for UML/OCL where corresponding approaches have been investigated only recently. Besides that, several approaches for the verification of the behavior specified in UML/OCL models have been proposed. They rely on a symbolic representation of all possible system states and transitions between them. But here, frame conditions have not been considered yet - a significant drawback for the underlying verification approaches. In this paper, we describe how to integrate frame conditions to symbolic representations. This enables designers to verify the behavior of UML/OCL models while, at the same time, respecting the given frame conditions.

In this article, we introduce a novel method of synthesizing symmetric Boolean functions with reversible logic gates. In contrast to earlier approaches, the proposed technique deploys a simple, regular, and cascaded structure consisting of an array of Peres and CNOT gates, which results in significant reduction with respect to the quantum cost. However, the number of circuit inputs may increase slightly when such cascades are used. In order to reduce their number, we next propose a postsynthesis optimization phase that allows judicious reuse of circuit lines. In addition to offering a cost-effective synthesis methodology, the proposed reversible logic structure supports elegant testability properties. With respect to all single or partial missing gate faults (SMGFs and PMGFs), or repeated gate faults (RGFs) in such an n -input circuit module, we show that it admits a universal test set of constant cardinality (=3) for any value of n . Thus, considering both the cost and testability issues, this approach provides a superior option for synthesizing symmetric functions compared to existing designs.

Optical circuits are considered a promising emerging technology for applications in ultra-high-speed networks or interconnects. However, the development of (automatic) synthesis approaches for such circuits is still in its infancy. Although first generic and automatic synthesis approaches have been proposed, no clear understanding exists yet on how to keep the costs of the resulting circuits as small as possible. In the domain of optical circuits, this is particularly interesting for the number of gates and the effect of so-called splitters to the signal strength. In this work, we investigate this relation by considering a variety of (existing as well as proposed) synthesis approaches for optical circuits. Our investigations show that reducing the number of gates and reducing the number of splitters are contradictory optimization objectives. Furthermore, the performance of synthesis guided with respect to gate efficiency as well as synthesis guided with respect to splitter freeness is evaluated and an overhead factor between the contradictory metrics is experimentally determined.

Reversible logic represents the basis for many emerging technologies and has recently been intensively studied. However, most of the Boolean functions of practical interest are irreversible and must be embedded into a reversible function before they can be synthesized. Thus far, an optimal embedding is guaranteed only for small functions, whereas a significant overhead results when large functions are considered. We study this issue in this article. We prove that determining an optimal embedding is coNP-hard already for restricted cases. Then, we propose heuristic and exact methods for determining both the number of additional lines and a corresponding embedding. For the approaches, we considered sum of products and binary decision diagrams as function representations. Experimental evaluations show the applicability of the approaches for large functions. Consequently, the reversible embedding of large functions is enabled as a precursor to subsequent synthesis.

Test compaction is an important aspect in the post-production test since it is able to reduce the test data and the test costs, respectively. Current automatic test pattern generation (ATPG) methods treat all faults independently from each other which limits the test compaction capability. We propose a new optimization satisfiability (SAT)-based ATPG for compact test set generation with high fault coverage as well as a new retargeting stage for test set reduction. The ATPG is based on a novel multiple-target test generation formulation using optimization techniques. Robust SAT-based solving algorithms are leveraged to determine compatible fault groups which can be detected by the same test. The proposed technique can be used during initial compact test generation as well as a post-process to increase the compactness of existing test sets, e.g., generated by commercial tools, in an iterative manner. Experimental results show that the proposed SAT-based approach is able to produce highly compacted test sets with high fault coverage for stuck-at as well as transition faults. The approach is able to produce lower pattern counts than a commercial ATPG tool. For one industrial circuit, the test set size can even be reduced down to 26% of the size generated by a commercial ATPG tool.

Quantum mechanical phenomena such as phase shifts, superposition, and entanglement show promise in use for computation. Suitable technologies for the modeling and design of quantum computers and other information processing techniques that exploit quantum mechanical principles are in the range of vision. Quantum algorithms that significantly speed up the process of solving several important computation problems have been proposed in the past. The most common representation of quantum mechanical phenomena are transformation matrices. However, the transformation matrices grow exponentially with the size of a quantum system and, thus, pose significant challenges for efficient representation and manipulation of quantum functionality. In order to address this problem, first approaches for the representation of quantum systems in terms of decision diagrams have been proposed. One very promising approach is given by Quantum Multiple-Valued Decision Diagrams (QMDDs) which are able to efficiently represent transformation matrices and also inherently support multiple-valued basis states offered by many physical quantum systems. However, the initial proposal of QMDDs was lacking in a formal basis and did not allow, e.g., the change of the variable order-an established core functionality in decision diagrams which is crucial for determining more compact representations. Because of this, the full potential of QMDDs or decision diagrams for quantum functionality in general has not been fully exploited yet. In this paper, we present a refined definition of QMDDs for the general quantum case. Furthermore, we provide significantly improved computational methods for their use and manipulation and show that the resulting representation satisfies important criteria for a decision diagram, i.e., compactness and canonicity. An experimental evaluation confirms the efficiency of QMDDs.

Motivated by the promises of significant speed-ups for certain problems, quantum computing received significant attention in the past. While much progress has been made in the development of synthesis methods for quantum circuits, new physical developments constantly lead to new constraints to be addressed. The limited interaction distance between the respective qubits (i.e. nearest neighbor optimization) has already been considered intensely. But with the emerge of multi-dimensional quantum architectures, new physical requirements came up for which only a few automatic synthesis solutions exist yet all of them of heuristic nature. In this work, we propose an exact scheme for nearest neighbor optimization in multi-dimensional quantum circuits. Although the complexity of the problem is a serious obstacle, our experimental evaluation shows that the proposed solution is sufficient to allow for a qualitative evaluation of the respective optimization steps. Besides that, this enabled an exact comparison to heuristical results for the first time.

With the advancements in silicon photonics, optical devices have found applications e.g. for ultra-high speed and low-power interconnects as well as functional computations to be realized on-chip. Caused by the increasing complexity of the underlying functionality, also the need for computer-aided design methods for this technology rises. Motivated by that, initial work on the development of synthesis methods for optical circuits has been performed. But all approaches proposed thus far suffer e.g. from unsatisfactory synthesis results or restricted scalability. In particular, splittings in the resulting circuits which degrade the optical signals into hardly measurable fractions prevent an efficient and scalable synthesis for optical circuits. In this work, we present a synthesis approach based on Binary Decision Diagrams (BDDs) that overcomes these obstacles. The approach yields circuits that rely on a total of zero splitters - at the expense of a moderate increase in the number of optical gates. Experiments confirm that, by this, an efficient and scalable synthesis scheme for optical circuits eventually becomes available.

Formal verification of high-level SystemC designs is an important and challenging problem. Recent works have proposed symbolic simulation in combination with Partial Order Reduction (POR) as a promising solution and experimentally demonstrated its potential. However, these symbolic simulation approaches have a fundamental limitation in handling cyclic state spaces. The reason is that they are based on stateless model checking and thus unable to avoid revisiting states in a cycle. In this paper, we propose a novel stateful symbolic simulation approach for SystemC. For the efficient detection of revisited symbolic states, we apply symbolic subsumption checking. Furthermore, our implementation integrates a cycle proviso to preserve the soundness of POR in the presence of cycles. We demonstrate the scalability and the efficiency of the proposed approach using an extensive set of experiments.

The complexity of today's embedded and cyber-physical systems is rapidly increasing and makes the consideration of higher levels of abstraction during the design process inevitable. In this context, the impact of modeling languages such as UML and its profiles such as MARTE is growing. Here, CCSL provides a formal description of timing constraints which have to be enforced on the considered system. This builds the basis for many further design steps and can be used e. g. for checking the consistency of the specification, for code generation, or for proving whether the time constraints have correctly been implemented at lower abstraction levels. However, most of the approaches available thus far usually focus on sole design tasks only -- often even without an explicit consideration of the system's functional behavior. In this work, we are aiming for overcoming this drawback by providing a method to automatically generate a generic representation of a set of clock constraints in terms of a transition relation. Afterwards, the resulting transition relation can easily be utilized for the above mentioned design tasks. A discussion on the applicability of the generic description as well as an exemplary evaluation shows the promise of the proposed generic representation.

The design of modern hardware systems is a very complex and time consuming process. At the beginning of the design process, requirements need to be specified. Errors in that early design stage derived by misinterpretation of the requirements can be hard to detect and require significant effort and costs to get fixed. To prevent errors, requirements should be written in a comprehensive and unambiguous way. Thus, designers are interested in automatic assistance tools that help writing better requirements. Conventional approaches are usually rule-based, thus many syntactic and semantic properties are not considered. In this paper we introduce an alternative approach to ensure the quality of requirements. The approach has two stages and assists the designer by providing (i) all relevant statistics about the syntactic and semantic properties of the sentence, and (ii) a single consolidated nominal quality predicate for the sentence such as good, medium, or bad. Although such statistical quality assessment leads to already satisfying results, the algorithm prediction reliability can further be enhanced by machine learning techniques. The achieved reliability for quality assessment in combination with the overview of the metrics about syntax and semantic can help the designer to write more comprehensive and less ambiguous requirements.

Modeling languages such as UML or SysML in combination with constraint languages such as OCL allow for an abstract description of a system prior to its implementation. But the resulting system models can be highly non-trivial and, hence, errors in the descriptions can easily arise. In particular, too strong restrictions leading to an inconsistent model are common. Motivated by this, researchers and engineers developed methods for the validation and verification of given formal models. However, while these methods are efficient to detect the existence of an inconsistency, the designer is usually left alone to identify the reasons for it. In this contribution, we propose an automatic method which efficiently determines reasons explaining the contradiction in an inconsistent UML/OCL model. For this purpose, all constraints causing the contradiction are comprehensibly analyzed. By this, the designer is aided during the debugging of his/her model.

For the development of complex systems - composed of hardware, software, or both - more and more high-level descriptions have been introduced over the past years. Starting from an informal specification, models of the system are created with the help of languages such as UML, SysML, or MARTE. Based on this model, an implementation is generated in a programming language such as C++, Java, etc. for software or SystemC, VHDL, etc. for hardware. Whereas various approaches for the verification of the single levels of abstraction exist, their application to a cross-level design flow is still to be considered. In this work, we evaluate this issue by providing a case study on a verification-driven design across abstraction levels. The results of this case study demonstrate the capabilities of existing methods as well as challenges and open issues to be addressed in future work.

Formal models, based on modeling languages such as UML in combination with constraint languages such as OCL, allow for an abstract description of a system prior to its implementation. But since the resulting models are often rather complex, redundancies in terms of model descriptions which can directly be implied from already existing constraints can easily arise. In particular, OCL invariants are affected by this. In order to efficiently detect those, methodologies for the analysis for invariant dependence have recently been proposed. However, they have severe limitations with respect to scalability, automation, and quality of the determined results. In this work, we aim for leveraging the analysis for invariant independence in formal systems models by addressing these drawbacks. For this purpose, a new methodology based on the exploitation of powerful solving engines as well as a complete analysis scheme is proposed. Experimental evaluations confirm that the proposed solution is significantly faster and leads to a much better quality of the results.

Reverse engineering is the extraction of word level information from a gate-level netlist. It has applications in formal verification, hardware trust, information recovery, and general technology mapping. A preprocessing step finds blocks in a circuit in which word level components are expected. A second step searches for word level components in these blocks. For this second step, we propose two variants of equivalence checking that consider subfunction containment. We propose algorithms to solve these variants by using subgraph isomorphism. A simulation graph (SG) is constructed for the block and for each library component, using a set of permutation-invariant simulation vectors for that component. If a library component SG is a subgraph of the block SG, we have a candidate match, which is then checked by standard equivalence checking. We extend a state-of-the-art subgraph isomorphism algorithm, LAD, to handle simulation graphs efficiently and also propose a SAT-based formulation. Experimental evaluations show that our algorithms can efficiently find 32-bit arithmetic components in blocks with over 300 primary inputs.

Binary Decision Diagrams (BDDs) are widely used in electronic design automation and formal verification. BDDs are a canonical representation of Boolean functions with respect to a variable ordering. Finding a variable ordering resulting in a small number of nodes and paths is a primary goal in BDD optimization. There are several approaches minimizing the number of nodes or paths in BDDs, but yet no method has been proposed to minimize both objectives at the same time.

Advances in microfluidic technologies have led to the emergence of Digital Microfluidic Biochips (DMFBs), which are capable of automating laboratory procedures in biochemistry and molecular biology. During the design and use of these devices, droplet routing represents a particularly critical challenge. Here, various design tasks have to be addressed for which, depending on the corresponding scenario, different solutions are available. However, all these developments eventually result in an “inflation” of different design approaches for routing of DMFBs - many of them addressing a very dedicated routing task only. In this work, we propose a comprehensive routing methodology which (1) provides one (generic) solution capable of addressing a variety of different design tasks, (2) employs a “push-button”-scheme that requires no (manual) composition of partial results, and (3) guarantees minimality e.g., with respect to the number of timesteps or the number of required control pins. Experimental evaluations demonstrate the benefits of the solution, i.e., the applicability for a wide range of design tasks as well as improvements compared to specialized solutions presented in the past.

Formal methods advanced to an important core technique in Computer-Aided Design (CAD). At the same time, researchers and engineers also started the investigation of so-called emerging technologies such as reversible computation, quantum computation, or optical circuits. Although most of these technologies are still in a rather “academic” state, first physical realizations have already been presented. This motivates a more detailed consideration of how to design circuits for these technologies. As for conventional circuits, formal methods do play an important role here. In this tutorial paper1, we are aiming to address the current momentum caused by the recent accomplishments and provide an overview of these emerging technologies as well as their corresponding CAD methods. This includes a special focus on how formal methods may help in the design and verification of circuits for those technologies.

The Unified Modeling Language (UML) is a defacto standard for software development and, together with the Object Constraint Language (OCL), allows for a precise description of a system prior to its implementation. At the same time, these descriptions can be employed to check the consistency and, hence, the correctness of a given UML/OCL model. In the recent past, numerous (automated) approaches have been proposed for this purpose. The behavior of the systems has usually been considered by means of sequence diagrams, state machines, and activity diagrams. But with the increasing popularity of design by contract, also composite structures, classes, and operations are frequently used to describe behavior in UML/OCL. However, for these description means no solution for the validation and verification of concurrent behavior is available yet. In this work, we propose such a solution. To this end, we discuss the possible interpretations of “concurrency” which are admissible according to the common UML/OCL interpretation and, afterwards, propose a methodology which exploits solvers for SAT Modulo Theories (i. e., SMT solvers) in order to check the concurrent behavior of UML/OCL models. How to address the resulting problems is described and illustrated by means of a running example. Finally, the application of the proposed method is demonstrated.

The application of built-to-order embedded hardware designs in safety critical systems requires a high design quality and robustness during operation. Flawless execution of the involved software can be compromised by malfunctioning hardware components or by software-induced errors. Furthermore, intellectual property (IP) tends to become unavoidable in modern hardware designs. Any unexpected behavior of IP components may cause unrecoverable system errors. In order to construct correct and safe systems from unverified and potentially malicious components, we propose a system integration approach which encapsulates IP blocks in verifiable container modules. The synthesis of these container modules is driven by a domain specific language (DSL) augmented with sequential extended regular expressions (SEREs). The approach is demonstrated by showing the synthesis of an effective countermeasure against software-induced memory disturbance errors.

This paper presents a rule based approach to optimize the quantum cost of reversible circuits using circuit rewriting rules that handle positive and negative controls. Since incremental optimization cannot guarantee optimality, we consider the application of simulated annealing to find further sub-circuits that could be replaced with smaller ones. Experimental evaluations show that simulated annealing not only can significantly improve the quality of reversible circuits but also is more efficient than a comparable greedy approach. Using the rewriting rules combined with the proposed method quantum cost reductions by up to 80% can be achieved.

Quantum circuits established themselves as a promising emerging technology and, hence, attracted considerable attention in the domain of computer-aided design. As a result, many approaches for synthesis of corresponding netlists have been proposed in the last decade. However, as the design of quantum circuits faces serious obstacles caused by phenomena such as superposition, entanglement, and phase shifts, automatic synthesis still represents a significant challenge. In this paper, we propose an automatic synthesis approach for quantum circuits that implement Clifford Group operations. These circuits are essential for many quantum applications and cover core aspects of quantum functionality. The proposed approach exploits specific properties of the unitary transformation matrices that are associated to quantum operations. Furthermore, Quantum Multiple-Valued Decision Diagrams (QMDDs) are employed for an efficient representation of these matrices. Experimental results confirm that this enables a compact realization of the respective quantum functionality.

Motivated by its promising applications e.g. for database search or factorization, significant progress has been made in the development of automated design methods for quantum circuits. But in order to keep up with recent physical developments in this domain, new technological constraints have to be considered. Limited interaction distance between gate qubits is one of the most common of these constraints. This led to the development of several strategies aiming at making a given quantum circuit nearest neighbor-compliant by inserting SWAP gates into the existing structure. Usually these strategies are of heuristic nature. In this work, we present an exact approach that enables nearest neighbor-compliance by inserting a minimal number of SWAP gates. Experiments demonstrate the applicability of the approach which enabled a comparison of results obtained by heuristic methods to the actual optimum.

With the advances of the microfluidic technology, the design of digital microfluidic biochips recently received significant attention. But thus far, the corresponding design tasks such as binding, scheduling, placement, and routing have usually been considered separately. Furthermore, often just heuristic results have been obtained. In this work, we present a one-pass synthesis scheme which directly realizes the desired functionality onto the chip and, at the same time, guarantees minimality with respect to area and/or timing. For this purpose, the deductive power of solvers for Boolean satisfiability is exploited. Experiments show how the approach leverages the design of the respective devices.

Intelligent automotive electronics significantly improved driving safety in the last decades. With the increasing complexity of automotive systems, dependability of the electronic components themselves and of their interaction must be assured to avoid any risk to driving safety due to unexpected failures caused by internal or external faults.

With increasing design complexity System on Chip (SoC) verification is becoming a more and more important and challenging aspect of the overall development process. The Universal Verification Methodology (UVM) is thereby a common solution to this problem; although it still keeps some problems unsolved. In this panel leading experts from industry (both users and vendors) and academy will discuss the future of SoC verification methodology.

Ensuring the correctness of high-level SystemC designs is an important and challenging problem in today's Electronic System Level (ESL) methodology. Prevalently, a design is checked against a functional specification given by e.g. a testcase with reference output or a user-defined property. Another research direction takes the view of a SystemC design as a piece of concurrent software. The design is then checked for common concurrency problems and thus, a functional specification is not required. Along this line, several methods for deadlock detection and race analysis have been developed. In this work, we propose to consider a new concurrency verification problem, namely input-output determinism, for Sys-temC designs. That means for each possible input, the design must produce the same output under any valid process schedule. We argue that determinism verification is stronger than both deadlock detection and race analysis. Beside being an attractive correctness criterion itself, proven determinism helps to accelerate both simulative and formal verification. We also present a preliminary study to show the feasibility of determinism verification for SystemC designs.

Synthesis of reversible circuits has attracted the attention of many researchers. In particular, approaches based on Decision Diagrams (DDs) have been shown beneficial since they enable the realization of corresponding circuits for large functions. However, all existing approaches rely on a gate library composed of positive control lines only. Recently, it has been shown that the additional use of negative control lines enables significant reductions of the respective circuit costs. In this paper, we aim for exploiting this potential. To this end, two complementary schemes are investigated. First, a post-synthesis optimization that exploits the power of negative control lines is utilized to optimize the circuits generated by previously proposed DD-based methods. Second, negative control lines are explicitly considered during synthesis. Experimental results demonstrate that the proposed approaches result in a significant reduction with respect to gate count as well as quantum costs.

Simulation-based verification is still the most frequently used technique when complex designs are to be verified. Stimuli are thereby generated and applied in order to sufficiently trigger and, by this, verify a set of considered scenarios. In general, a scenario can be triggered in various fashions. To ensure a high verification quality, each of these fashions should adequately be covered. However, to the best of our knowledge, this has not appropriately been addressed thus far, i.e. existing stimuli generation is mainly performed without an explicit consideration of the possible fashions in which a scenario might be triggered. To improve this, three approaches are proposed in this work. While examples illustrate their advantages, a case study confirms that, using the proposed approaches, very compact sets of stimuli satisfying this coverage requirement can efficiently be generated.

Test compaction is an important aspect in the postproduction test since it is able to reduce the test data and the test costs, respectively. Current ATPG methods treat all faults independently from each other which limits the test compaction capability. This paper proposes a new optimization based SAT-ATPG for compact test set generation. Robust solving algorithms are leveraged to determine fault groups which can be detected by the same test. The proposed technique can be used during initial compact test generation as well as a post-process to increase the compactness of existing test sets, e.g, generated by commercial tools, in an iterative manner. Experimental results on industrial circuits and academic benchmarks show that this technique is able to significantly reduce the pattern count down to 40% for the initial test generation and down to 30% for the iterative reduction.

Modeling languages such as SysML provide various description means for a precise specification of the desired system. As a system model typically uses multiple diagram types focusing on different aspects, it is crucial to keep them consistent to each other. In this paper, we propose a verification methodology which ensures the consistency between activity diagrams as blueprints for the implementation and their contracts from a block definition diagram. For this purpose, activity diagrams are transformed to OCL constraints that can be checked against pre- and postconditions. The proposed approach is evaluated in a case study based on an industrial specification.

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

For the design of complex systems, formal modeling languages such as UML or SysML find significant attention. The typical model-driven design flow assumes thereby an initial (abstract) model which is iteratively refined to a more precise description. During this process, new errors and inconsistencies might be introduced. In this paper, we propose an automatic method for verifying the consistency of refinements in UML or SysML. For this purpose, a theoretical foundation is considered from which the corresponding proof obligations are determined. Afterwards, they are encoded as an instance of Satisfiability Modulo Theories (SMT) and solved using proper solving engines. The practical use of the proposed method is demonstrated and compared to a previously proposed approach.

In order to verify natural language assertions from a specification automatically, they need to be translated into formal representations. This process is error-prone and can lead to a product that does not meet the initial intentions.We automate this process by first partitioning all assertions into subsets based on sentence similarity and then providing a translation template for each subset which must be completed by the designer. Since many assertions are described by similar sentences, the number of manual translation steps can be decreased significantly. We evaluated our approach by translating English constraint sentences from an industrial specification into SystemVerilog assertions.

This tutorial paper summarizes selective research results from the field of automated requirement engineering. Automatization is achieved by employing natural language processing techniques. We show algorithms that work directly on the natural language text and algorithms that translate natural language text to formal models. To ensure quality, we further illustrate verification algorithms that can proof correctness of the extracted formal models.

Digital microfluidic biochips enable a higher degree of automation in laboratory procedures in biochemistry and molecular biology and have received significant attention in the recent past. Their design is usually conducted in several stages with routing being a particularly critical challenge. Previously proposed solutions for this design step suffer from two issues: They are mainly of heuristic nature and usually assume that the blockages to be bypassed are present the entire time. In contrast, we present a methodology which exploits the fact that blockages are often only present at certain intervals. At the same time, our approach guarantees exact solutions, i.e. always determines a routing with a minimal number of time steps. Experimental results show that, despite the huge complexity, optimal results can be achieved in reasonable run-time and that the consideration of temporary blockages indeed significantly improves the routing results.

Due to the increasing complexity of today's embedded systems, the design on higher levels of abstraction becomes more and more important. In this context, modeling languages such as UML and its profile MARTE received significant attention in the recent past. They provide formal descriptions that can be exploited to automatically generate initial implementations of a system e.g. In SystemC. While corresponding approaches have been developed in the past, they often focused on functional specifications. Besides that, also non-functional behavior such as clocking constraints needs to be considered in this process. In this work, we propose an approach which addresses this gap. Given a formal specification of clocking constraints specified in the Clock Constraint Specification Language (CCSL, a MARTE accessory), we propose an automatic code generation scheme which enriches an existing SystemC implementation by a module triggering the desired clocks in the system.

No abstract available.

Research in the domain of quantum computation is mainly driven by their promising applications e.g., for factorization or database search. At the same time, physical developments for this emerging technology constantly lead to new constraints to be addressed by logic designers. The limited interaction distance between qubits, the elementary information storage in quantum circuits, is one of the most common restrictions, leading to the fact that, for many quantum architectures, computations can only be performed on adjacent (i.e., nearest neighbor) qubits. Motivated by that, optimization of quantum circuits with respect to this restriction has become an intensely considered research topic. In this paper, we briefly review existing approaches that have been proposed in the past for this purpose. We particularly consider that almost all existing solutions are of heuristic nature, i.e., do not guarantee an optimal solution. In order to address this, exact alternatives are introduced which make use of the deductive power of constraint solvers. By this, we are able to perform a qualitative evaluation of the performance of existing (heuristic) solutions for linear nearest neighbor quantum circuit optimization.

The efficient synthesis of quantum circuits is an active research area. Since many of the known quantum algorithms include a large Boolean component (e.g. the database in the Grover search algorithm), quantum circuits are commonly synthesized in a two-stage approach. First, the desired function is realized as a reversible circuit making use of existing synthesis methods for this domain. Afterwards, each reversible gate is mapped to a functionally equivalent quantum gate cascade. In this paper, we propose an improved mapping of reversible circuits to quantum circuits which exploits a certain structure of many reversible circuits. In fact, it can be observed that reversible circuits are often composed of similar gates which only differ in the position of their target lines. We introduce an extension of reversible gates which allow multiple target lines in a single gate. This enables a significantly cheaper mapping to quantum circuits. Experiments show that considering multiple target lines leads to improvements of up to 85% in the resulting quantum cost.

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.

Modeling languages such as UML or SysML received significant attention over the last years. They allow for an abstract description of systems already in the absence of a precise implementation or a hardware/software partitioning. Additionally considering textual constraints, for example provided by means of OCL, enables to automatically check the specified systems e.g. for consistency of the structure or reachability of certain system states. However, for the majority of verification tasks, not the entire model has to be considered. In this work, we propose an approach that automatically determines reduced system models, i.e. system descriptions that only include model elements which are relevant for the considered verification task. Considering reduced models eases the access by the designer and supports incremental design and verification schemes. But most important, they improve the efficiency of the applied formal verification engine. Experiments demonstrate that already small reductions in the model lead to significant accelerations in the run-time of the verification engine.

The use of modeling languages such as UML or SysML enables to formally specify and verify the behavior of digital systems already in the absence of a specific implementation. However, for each modeling method and verification task usually a separate verification solution has to be applied today. In this paper, a methodology is envisioned that aims at stopping this “inflation” of different verification approaches and instead employs a generic methodology. For this purpose, a given specification as well as the verification shall be transformed into a basic model which itself is specified by means of a generic modeling language. Then, a range of automatic reasoning engines shall uniformly be applied to perform the actual verification. A feasibility study demonstrates the applicability of the envisioned approach.

Modern systems consisting of hardware and software are becoming more and more complex. The underlying data of next generation systems will consist of billions of entries in terms of components or lines of code. Handling this data efficiently is one of the major challenges for future EDA. In order to provide a meaningful preparation for these complex issues it is inevitable to deal with highly elaborated visualization techniques. It is unimaginable how data sets of this size could be grasped without advanced plotting methods. Although a lot of effort has been put into research for visualization of hardware and software, techniques hardly exist that consider them in combination. Besides that, in most cases visualization techniques concentrate on the illustration of the system's structure and behavior, e.g. to ease debugging. However, far more information can be integrated. As an example, in the context of verification the accentuation of coverage metrics on top of the structural visualization of a system would immediately pinpoint the verification engineer to areas that are poorly validated. Furthermore, when considering the co-design of hardware-software systems, design exploration can be carried out much easier when the designer gets immediate visual feedback. Inspired by recent achievements in visualization methods and the invention of sophisticated machinery, in this invited paper we propose the use of Hardware-Software Co-Visualization (HSCV). The potential of current techniques as well as their limitations will be demonstrated. Furthermore, we are seeking for alternative methods in system visualization that go beyond monitors and printed pages. Techniques from 3D rendering and virtual reality are utilized for this purpose leading to a holistic environment in which complex systems can be grasped within seconds just as huge data sets in the context of plots. State-of-the-art is presented and directions for future work are outlined.

Cone of influence analysis, i.e. determining the parts of the circuit which are relevant to a considered circuit signal, is an established methodology applied in several design tasks. In abstractions like the Register Transfer Level (RTL) or the gate level, cone of influence analysis is simple. However, the introduction of higher levels of abstractions, particularly the Electronic System Level (ESL), made it significantly harder to reliably extract a cone of influence. In this paper, we propose a methodology that enables cone of influence analysis at the ESL. Instead of a structural analysis, a behavioral scheme is proposed, i.e. stimuli representing different system executions are analyzed. To this end, machine learning techniques are exploited. This enables a very good approximation of the desired cone of influence which is non-invasive, does not rely on the availability of the source code, and performs fast. Case studies confirm the applicability of the proposed approach.

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.

Automatic Test Pattern Generation (ATPG) based on Boolean Satisfiability (SAT) is a robust alternative to classical structural ATPG. Due to the powerful reasoning engines of modern SAT solvers, SAT-based algorithms typically provide a high test coverage because of the ability to reliably classify hard-to-detect faults. However, a drawback of SAT-based ATPG is the test compaction ability. In this paper, we propose an enhanced dynamic test compaction approach which leverages the high implicative power of modern SAT solvers. Fault detection constraints are encoded into the SAT instance and a formal optimization procedure is applied to increase the detection ability of the generated tests. Experiments show that the proposed approach is able to achieve high compaction - for certain benchmarks even smaller test sets than the currently best known results are obtained.

Reversible circuits are an emerging technology where all computations are performed in an invertible manner. Motivated by their promising applications, e.g. in the domain of quantum computation or in the low-power design, the synthesis of such circuits has been intensely studied. However, how to automatically realize reversible circuits with the minimal number of lines for large functions is an open research problem. In this paper, we propose a new synthesis approach which relies on concepts that are complementary to existing ones. While “conventional” function representations have been applied for synthesis so far (such as truth tables, ESOPs, BDDs), we exploit Quantum Multiple-valued Decision Diagrams (QMDDs) for this purpose. An algorithm is presented that performs transformations on this data-structure eventually leading to the desired circuit. Experimental results show the novelty of the proposed approach through enabling automatic synthesis of large reversible functions with the minimal number of circuit lines. Furthermore, the quantum cost of the resulting circuits is reduced by 50% on average compared to an existing state-of-the-art synthesis method.

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.

In model-based design, it is common and helpful to use invariants in order to highlight restrictions or to formulate characteristics of a design. In contrast to pre- and post-conditions, they represent global constraints. That is, they are harder to explicitly consider and, thus, become disadvantageous when the design process approaches the implementation phase. As a consequence, they should be removed from a design when it comes to an implementation. However, so far only naïve tool support aiding the designer in this task is available. In this paper, we present an approach which addresses this problem. A methodology is proposed which iteratively removes invariants from a model and, afterwards, presents the designer with invalid scenarios originally prevented by the just eliminated invariant. Using this, the designer can either manually modify the model or simply take the automatically generated suggestion. This enables to entirely eliminate all invariants without changing the semantics of the model. Case studies illustrate the applicability of the proposed approach.

The application of coding strategies is an established methodology to improve the characteristics of on-chip interconnect architectures. Therefore, design methods are required which realize the corresponding encoders and decoders with as small as possible overhead in terms of power and delay. In the past, conventional design methods have been applied for this purpose.

While being a de-facto standard for the modeling of software systems, the Unified Modeling Language (UML) is also increasingly used in the domain of hardware design and hardware/software co-design. To ensure the correctness of the specified systems, approaches have been presented which automatically verify whether a UML model is consistent, i.e. free of conflicts. However, if the model is inconsistent, these approaches do not provide further information to assist the designer in finding the error. In this work, we present an automatic debugging approach which determines contradiction candidates, i.e. a small subset of the original model explaining the conflict. These contradiction candidates aid the designer in finding the error faster and therefore accelerate the whole design process. The approach employs different satisfiability solvers as well as different debugging strategies. Experimental results demonstrate that, even for large UML models with up to 2500 classes and constraints, the approach determines a very small number of contradiction candidates to be inspected.

The test set size is a highly important factor in the post-production test of circuits. A high pattern count in the test set leads to long test application time and exorbitant test costs. We propose a new test generation approach which has the ability to reduce the test set size significantly. In contrast to previous SAT-based ATPG techniques which were focused on dealing with hard single faults, the proposed approach employs the robustness of SAT-solvers to primarily push test compaction. Furthermore, a concept is introduced how the novel technique can be flexibly integrated into an existing industrial flow to reduce the pattern count. Experimental results on large industrial circuits show that the approach is able to reduce the pattern count of up to 63% compared to state-of-the-art dynamic compaction techniques.

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.

Reversible circuits rely on an entirely different computing paradigm allowing to perform computations not only from the primary inputs to the primary outputs but also vice versa. Recently, first physical realizations based on this paradigm have been introduced in the domain of quantum computation and low-power circuits. This puts key test challenges for the future on the table. While first steps towards testing such circuits have been made (e.g. fault models and appropriate ATPG methods have been introduced), fault diagnosis has hardly been considered so far. In this paper, we consider the application of fault diagnosis methods for reversible circuits. In particular, we propose a new fault diagnosis approach which explicitly exploits the advantageous properties of reversible circuits. Experiments show that even though conventional methods can be applied to reversible circuits, improvements of more than one order of magnitude are achieved if reversibility is explicitly exploited.

Delay testing is performed to guarantee that a manufactured chip is free of delay defects and meets its performance specification. However, only few delay faults are robustly testable. For robustly untestable faults, non-robust tests which are of lesser quality are typically generated. Due to significantly relaxed conditions, there is a large quality gap between non-robust and robust tests. This paper presents a test generation procedure for As-Robust-As-Possible (ARAP) tests to increase the overall quality of the test set. Instead of generating a non-robust test for a robustly untestable fault, an ARAP test is generated which maximizes the number of satisfiable conditions required for robust test generation by pseudo-Boolean optimization. Additionally, the problem formulation is extended to incorporate the increased significance of small delay defects. By this, the likeliness that small delay defects invalidate the test is reduced. Experimental results on large industrial circuits confirm the quality gap and show that the generated ARAP tests satisfy a large percentage of all robustness conditions on average which signifies a very high quality.

The Unified Modeling Language (UML) as a defacto standard for software development finds more and more application in the design of systems which also contain hardware components. Guaranteeing the correctness of a system specified in UML is thereby an important as well as challenging task. In recent years, first approaches for this purpose have been introduced. However, most of them focus only on the static view of a UML model. In this paper, an automatic approach is presented which checks verification tasks for dynamic aspects of a UML model. That is, given a UML model as well as an initial system state, the approach proves whether a sequence of operation calls exists so that a desired behavior is invoked. The underlying verification problem is encoded as an instance of the satisfiability problem and subsequently solved using a SAT Modulo Theory solver. An experimental evaluation confirms the applicability of the proposed approach.

Synthesis of reversible circuits is an active research area motivated by its applications e.g. in quantum computation or low-power design. The number of used circuit lines is thereby a crucial criterion. In this paper, we introduce several methods (including a theoretical upper bound) for the efficient computation or at least approximation of the minimal number of lines needed to realize a given function in reversible logic. While the proposed exact approach requires a significant amount of run-time (exponential in the worst case), the heuristic methods lead to very precise approximations in very short run-time. Using this, it can be shown that current synthesis approaches for large functions are still far away from producing optimal circuits with respect to the number of lines.

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.

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

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.

ATPG based on Boolean satisfiability (SAT) turned out to be a robust alternative to classical structural automatic test pattern generation (ATPG) algorithms performing very well especially for hard-to-detect faults but suffer from the overhead for easy-to-detect faults. In this letter, we propose new efficient data structures and methodologies for SAT-based ATPG. The novel incremental SAT solving technique dynamic clause activation which makes use of structural information using dedicated data structures forms the core of a new flexible SAT-based ATPG approach. Experimental results on large industrial circuits show a significant performance gain and a removal of the limitations. At the same time, the robustness of SAT-based ATPG can even be strengthened resulting in very high fault efficiency and increased fault coverage for transition faults.

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

Reversible logic became a promising alternative to traditional circuits because of its applications e.g. in low-power design and quantum computation. As a result, design of reversible circuits attracted great attention in the last years. The number of circuit lines is thereby a major criterion since it e.g. affects the still limited resource of qubits. Nevertheless, all approaches introduced so far for synthesis of complex reversible circuits need a significant amount of additional circuit lines — sometimes orders of magnitude more than the primary inputs. In this paper, we propose a post-process optimization method that addresses this problem. The general idea is to merge garbage output lines with appropriate constant input lines. To this end, parts of the circuits are re-synthesized. Experimental results show that by applying the proposed approach, the number of circuit lines can be reduced by 17% on average — in the best case by more than 40%. At the same time, the increase in the number of gates and the quantum costs, respectively, can be kept small.

Nowadays, modeling languages like UML are essential in the design of complex software systems and also start to enter the domain of hardware and hardware/software codesign. Due to shortening time-to-market demands, ¿first time right¿ requirements have thereby to be satisfied. In this paper, we propose an approach that makes use of Boolean satisfiability for verifying UML/OCL models. We describe how the respective components of a verification problem, namely system states of a UML model, OCL constraints, and the actual verification task, can be encoded and afterwards automatically solved using an off-the-shelf SAT solver. Experiments show that our approach can solve verification tasks significantly faster than previous methods while still supporting a large variety of UML/OCL constructs.

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

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

In the past, reversible logic has become an intensely studied research topic. This is mainly motivated by its applications in the domain of low-power design and quantum computation. Since reversible logic is subject to certain restrictions (e.g. fanout and feedback are not allowed), traditional synthesis methods are not applicable and specific methods have been developed. In this paper, we focus on synthesis of multiplier circuits in reversible logic. Three methods are presented that address the drawbacks of previous approaches. In particular, the large number of circuit lines in the resulting realizations as well as the poor scalability. Finally, we compare the results to circuits obtained by general purpose synthesis approaches.

This paper considers the optimization of reversible and quantum circuits. Both represent the basis for emerging technologies e.g. in the area of quantum computation and low power design. An approach called window optimization is described that does not consider the circuit as a whole, but smaller sub-circuits of it (so called windows). Two schemes for extracting the windows and three approaches for their optimization are considered. Application scenarios show that applying the proposed optimizations leads to significant reductions of the circuit cost.

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

It was shown in the past that ATPG based on the Boolean Satisfiability problem is a beneficial complement to traditional ATPG techniques. Its advantages can be observed especially on large industrial circuits. These circuits usually contain a lot of functional redundancy which, on the one hand, is often needed during operational mode, but on the other hand, causes dispensable overhead during ATPG. Using the traditional circuit-to-CNF transformation, this redundancy is also contained in the SAT instances. The contribution of this paper is a new technique to improve the SAT instance generation for SAT-based ATPG. The objective of the proposed method is to use Binary Decision Diagrams (BDDs) to optimize the resulting CNF representations. In order to apply the proposed technique to industrial circuits, we developed dedicated BDD operations using a multiple-valued logic. The experimental results, obtained on large industrial designs, show that the accomplished optimizations result in a considerable acceleration of the overall ATPG runtime as well as in a significant reduction of the unclassified faults.