Deep Neural Networks (DNNs) are increasingly used in safety-critical Cyber-Physical Systems (CPS), requiring rigorous verification. Existing methods struggle with scalability and over-approximation. We introduce Affine Arithmetic Decision Diagrams (AADDs) for DNN reachability analysis, leveraging affine arithmetic to preserve variable correlations and improve precision. Our approach provides a structured symbolic representation of network decisions, enabling efficient and accurate verification. Additionally, AADDs unify verification for DNNs and Analog-Mixed-Signal (AMS) systems, supporting holistic safety analysis.

Behavioral models are used to describe the statistical behavior of subsystems that are too large for circuit simulation using SPICE. However, performance estimations obtained using these approaches are typically accurate only for relatively simple circuits, where the performance has a linear dependence on the variation parameters of the circuit. In this work, we introduce statistical performance models that employ piecewise linear regression (PWLR) to model circuit nonlinearity and interblock correlations for use within a hierarchical approach. Our algorithm uses sensitivity-based dimensionality reduction and k-means clustering to ensure that the nonlinear models for the circuit are efficient. The advantage of using PWLR models is illustrated using a current mirror and a charge pump under process, voltage and temperature (PVT) variations.

The paper reports on the industrial application of SystemC AMS for semi-symbolic analysis. As a case study we analyze the accuracy of a fuel consumption measurement system. As results, two approaches are presented that make formal and symbolic methods more accessible for industrial practice: (1) integration of symbolic simulation into SystemC AMS, which makes the application similar to the established concrete simulation, and (2) uncertainty tables to further simplify the remaining symbolic modeling of inputs and constraints.

We present a case study on virtual prototyping of automotive applications. We address the co-simulation of HW/SW systems involving firmware, communication protocols, and physical/mechanical systems in the context of model-based and agile development processes. The case study compares the Matlab/Simulink and SystemC based approaches by an e-gas benchmark. We compare the simulation performance, modeling capabilities and applicability in different stages of the development process.

This paper deals with the performance verification of analog/mixed-signal (AMS) systems by a mixed symbolic/numeric (nubolic) simulation. The approach is to piggyback the symbolic simulation via code-instrumentation on the existing, numeric SystemC AMS simulator. This permits the combination of symbolic and numeric simulation ("nubolic simulation"). The particular focus in the paper is the handling of the symbolic discrete-event process activations. This permits the symbolic simulation of digital parts of AMS systems modeled by discrete event processes. The approach is demonstrated by the symbolic simulation of a dual-charge-pump PLL of an IEEE 802.15.4 RF transceiver that includes an asynchronous digital counter as a frequency divider.

Formal methods are a promising alternative to simulation-based verification of mixed-signal systems. However, in practice, such methods fail to scale with heterogeneity and complexity of today's analog/mixed-signal systems. Furthermore, it is unclear how they can be integrated into existing verification flows. This paper shows a path to overcome these obstacles. The idea is to use a hierarchical verification flow, in which components can be verified by formal methods or by multirun simulation. To transport verification results across hierarchies, we represent parameters and properties by affine arithmetic decision diagrams. We study to which extent this approach fulfills the needs of practical application by the verification of a phase-locked loop of an IEEE 802.15.4 transceiver system.

Modeling languages first of all support simulation that is considered as reference by designers. Formal verification and synthesis share the same languages. However, they usually require a separate, dedicated compiler. As modeling languages such as SystemC have reached a high complexity, it is very hard to support reasonably large language subsets, and to guarantee consistency with simulation semantics. This paper shows a way to use the simulator itself to generate a formal model of the complete dynamic behavior. Compared with using yet another compiler, this permits to improve consistency with simulation semantics, and to combine simulation with other use-cases. We concretely focus on symbolic simulation of SystemC AMS ([1], [2], IEEE Std 1666.1-2016), for which we generate AADD and BDD for symbolic simulation.

On the contrary to the digital world, no coverage definition exists in the Analog/Mixed-Signal (AMS) context. As digital coverage helps digital designers and verification engineers to evaluate their verification progress, analog designers do not have such metrics. This paper proposes a set of different analog coverage metrics, which improve the confidence in AMS circuit verification. We will demonstrate, that no single overall coverage metric exists. However, as with digital coverage, the proposed analog coverage metrics could substantially help in rating the verification process. Illustrated by a complex AMS circuit example we will explore the limits of analog coverage methodologies as well as the benefits on different levels of abstraction ranging from transistor level up to system level.

The paper describes an approach for semi-symbolic analysis of mixed-signal systems that contain discontinuous functions, e.g. due to modeling comparators. For modeling and semi-symbolic simulation, we use extended Affine Arithmetic. Affine Arithmetic is currently limited to accurate analysis of linear functions and mild non-linear functions, but not yet discontinuities. In this paper we extend the approach to also handle discontinuities. For demonstration, we symbolically analyze a ΣΔ-modulator.

The increased design complexity of analog/mixed signal (AMS) systems puts a high pressure on researchers to find the efficient solutions for the verification of these systems. In contrast to digital designs, the nonlinear nature and higher sensitivity of AMS systems to parameter variations make the verification process more difficult. The focus of this paper is the verification of system robustness with respect to frequency and phase properties. For this purpose, the method, which combines simulation with assertion-based approach, is used. Assertions describing desired system properties use simulation results to verify the system behaviour. In order to provide more formal results using simulation-based methods, deviations of system parameters are modeled as ranges and superimposed to the nominal design model. The range-based representation of parameter values delivers formal model of AMS system for the considered parameter set. Hence, its simulation results in the range-based system response containing the set of simulation traces reachable for all parameter values lying in the specified ranges. The applicability and efficiency of the proposed simulation-based formal method is shown through the verification of PLL phase properties with respect to frequency.