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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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

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.

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.

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.

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.

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.

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.

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.