Training and running inference of large neural networks comes with excessive cost and power consumption. Thus, realizing these networks as analog circuits is an energy-and areaefficient alternative. However, analog neural networks suffer from inherent deviations within their circuits, requiring extensive testing for their correct behavior under these deviations. Unfortunately, tests based on Monte Carlo simulations are extremely time- and resource-intensive. We present an alternative approach to proving the correctness of the neural network using formal neural network verification techniques and developing a modeling methodology for these analog neural circuits. Our experimental results compare two methods based on reachability analysis showing their effectiveness by reducing the test time from days to milliseconds. Thus, they offer a faster, more scalable solution for verifying the correctness of analog neural circuits.

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.

The paper proposes a method for identifying undetectable defects in mixed-signal circuits to exclude them from further consideration in defect campaigns. The method uses an equivalence checker to generate counterexamples or prove the undetectability of a defect.

In this paper we present a method to debug and analyze large synthesized ANNs enabling a systematic comparison of the transistor netlist, behavioral model and the implementation. With that an insight into the behavior of the analog netlist is easily gained and errors during generation or badly designed cells are quickly uncovered. An overall judgement of the accuracy is also presented. We demonstrate the functionality on several examples from small ANNs to ANNs consisting of more than 10000 of cells implementing a medical application.

We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

Accurate abstracted behavioral modeling of analog circuits is still an open problem, especially when the abstraction process is automated. In this paper we present an automated abstraction technique of transistor level circuits with full SPICE accuracy alongside a significant simulation speed-up. The methodology computes a hybrid automaton which is transformed into a behavioral model in Verilog-A. The resulting hybrid automaton exhibits linear behavior as well as the technology dependent nonlinear e.g. limiting behavior. The accuracy and speed-up of the methodology is evaluated on several transistor level circuits ranging from simple operational amplifiers up to a complex industrial OTA-based Gm/C filter. Finally, we formally verify the equivalence between the generated model and the original circuit.

Mobility gets an increasing amount of meaning and significance in the modern society. In this paper, we introduce a multi-agent learning application for a multi-agent system in e-mobility. In particular, we propose a geospatial model for free-floating and autonomously driving e-trikes and demonstrate a calculation method of positioning e-trikes on a given area by using different methods of cluster analysis. The solution of the cluster analysis contains cluster centers which represent a positioning for the e-trikes. The solution is then evaluateded by a simulation model with more sophisticated parameters. This research field opens different opportunities of application scenarios, which are discussed in the conclusion.

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.

This paper proposes a systematic and fast analog coverage-driven verification methodology which could increase the confidence in verification of today's analog blocks. We define an appropriate coverage metric to score simulations and then minimize the simulation effort for achieving full state space coverage with an algorithm generating appropriate input stimuli. Our proposed method uses characteristic properties of a discretized representation of the state space such as the spatial distribution of eigenvalues, guiding the generation of short and purposeful stimuli. The experimental results show a significant speed-up with similar accuracy compared to the state-of-the-art.

This paper proposes a new methodology for automated analog circuit synthesis, aiming to address the challenges known from other analog synthesis approaches: unsatisfactory time predictability due to stochastic-driven circuit generation methods, the dereliction of the creative part during the design process, and the inflexibility leading to synthesis tools, which mostly only handle just one circuit class. This contribution presents the underlying concepts and ideas to provide the predictability, flexibility, and creative freedom in order to elevate analog circuit design to the next step. A circuit generation algorithm is presented, which allows a full design-space exploration. Furthermore, an isomorphism algorithm is developed, which reduces a given set of circuits to its unique being one of the first methodologies addressing this issue. Thus, the algorithm handles vast amounts of circuits in a very efficient manner. The results demonstrate the claimed feasibility and applicability of the synthesis framework in general and in the context of system design.

This paper proposes a novel modular architecture for Electrical Energy Storages (EESs), consisting of multiple series-connected cells. In contrast to state-of-the-art architectures, the presented approach significantly improves the energy utilization, safety, and availability of EESs. For this purpose, each cell is equipped with a circuit that enables an individual control within a homogeneous architecture. One major advantage of our approach is a direct and concurrent charge transfer between each cell of the EES using inductors. To enable a system-level modeling and performance analysis of the architecture, a detailed investigation of the components and their interaction with the Pulse Width Modulation (PWM) control was performed at transistor-level. At system-level, we propose a control algorithm for the charge transfer that aims at minimizing the energy loss and balancing time. The results give evidence of the significant advantages of our architecture over existing passive and active balancing methods in terms of energy efficiency and charge equalization time.

This contribution presents a major improvement for our analog synthesis framework with an explorative characteristic. The presented approach in principle allows the synthesis of a wide range of circuits, without the limitation to specific circuit classes. Defined by a specification of up to 15 different performances, a fully sized, transistor level circuit is synthesized for a provided process technology. The presented work reduces the needed computational effort and thus drastically reduces the synthesis time, while adding new abstraction into the framework to provide an even wider range of synthesized circuits - demonstrated in experimental results.

In this paper a novel approach to discrete state space modeling of nonlinear analog circuits is presented, based on the introduction of an underlying discrete analog transition structure (DATS) and the related optimization problem of accurately representing a nonlinear analog circuit with a DATS. Starting from a circuit netlist, a partitioning of the state space to the discrete model is generated parallel and orthogonal to the trajectories of the state space dynamics. Therefore, compared to previous approaches, a significantly higher accuracy of the model is achieved with a lower number of states. The mapping of the partitioning to a DATS enables the application of formal verification algorithms. Experimental validations show the soundness of the approach with an increase in accuracy between a factor of 4 to 10 compared to the state of the art. A model checking case study illustrates the application of the new discretization algorithm to identify a hidden circuit design error.

The Artificial Hormone System (AHS) is a self organizing system which allocates tasks to processing elements. It works in a distributed way, is able to hold real-time conditions and can run in a mixed-signal chip environment significantly increasing system reliability. Yet the hormone mechanisms offer new ways for malicious attacks which can affect the correct functioning of the AHS. Such attacks may cause severe damage if the AHS is used in an embedded (maybe real-time) environment. Therefore, this paper deals with analyzing malicious attacks on the AHS. We present several ways of attacking the AHS and resulting detection and defense strategies. We also evaluate these strategies in the paper and demonstrate that they can help to protect the AHS from attacks.

This contribution will present a fully automated approach for explorative topology synthesis of small analog circuit blocks. Circuits are composed from a library of basic building blocks. Therefore, various algorithms are used to explore the entire design space, even allowing to generate unusual circuits. Correct combination of the basic blocks is accomplished through generic electrical rules, which ensure the fundamental electrical functionality of the generated circuit. Additionally, symmetry constraints are introduced to narrow the design space, which leads to more reasonable circuits. Further a replaceable bias-voltage generator is included into the circuit to replicate real world circumstances. For the first evaluation and selection of best candidate circuits, fast symbolic analysis techniques are used. The final sizing is done through a parallelized industrial based sizing method. Experimental results show the feasibility of this synthesis approach.

This paper presents a tool for automatic analog topology generation and subsequent sizing. For this purpose a multistage design flow has been developed. To synthesize new circuit topologies according to a set of given specifications, a hierarchical algorithm composes the circuits using a library of basic building blocks. A set of constraints ensures an electrically reasonable interconnection of the blocks. In the next step all generated circuits are preselected by symbolic analysis methods. The following sizing is executed with SPICE accuracy. Three main extensions are applied, compared to previous approaches. First, the symbolic analysis methodology has been improved. Second, a yield optimization has been included to the sizing step. Third, an automated evaluation of hundreds successfully sized circuits is realized through searching for the pareto optimal designs. Results are shown through two different synthesis runs, generating operational amplifier topologies.

In this paper a comprehensive assertion-based verification methodology for the digital, analog and software domain of heterogeneous systems is presented. The proposed methodology combines a novel mixed-signal assertion language and the corresponding automatic verification algorithm. The algorithm translates the heterogeneous temporal properties into observer automata for a semi-formal verification. This enables automatic verification of complex heterogeneous properties that can not be verified by existing approaches. The experimental results show the integration of mixed-signal assertions into a simulation environment and demonstrate the broad applicability and the high value of the evolved solution.

In this contribution a novel methodology for verification of analog circuit blocks with the aim of full coverage of the analog state space is proposed. On a discretized state space model of the analog system, an efficient state space-guided input stimuli generation algorithm produces piecewise linear input stimuli for every input of the system under verification. Processed by a conventional transient circuit simulator, the simulation results are covering the system's complete dynamic behavior. Simulation by complete state space-covering input stimuli guarantees the verification results to be sound for every possible state and input stimulus of the circuit under verification, which increases the significance of property verification and equivalence checking of transistor netlists versus behavioral models. The application to example circuits shows the feasibility of the approach.

In this paper we firstly introduce a novel symbolic model checker (MScheck) for mixed-signal circuits.MScheckis capable to conflate the continuous behavior, typical for analog designs, and the discrete behavior in the digital domain for formal verification. Timing information of both systems will be symbolically stored within multi terminal binary decision diagrams (MTBDDs) for the entire verification procedure. The effectiveness of our approach is demonstrated on a phase locked loop (PLL) by formal verification of the locking property.

In this contribution an advanced methodology for model checking of analog systems is introduced. A new analog specification language (ASL)for efficient property specifications is defined and model checking algorithms for implementing this language are presented. This allows verification of complex static and dynamic circuit properties like oscillation and startup time that have not yet been formally verifiable with previous approaches. The new verification methodology is applied to example circuits and experimental results are discussed and compared to conventional circuit simulation.

This paper presents a method towards automatic structural synthesis of analog multiplier based on a hierarchical topology "super-topology", which is abstracted from the most standard four-quadrant multipliers. The essential components in the super-topology are four identical cells, which consist of several MOS-transistors and determine features and performances of multipliers. We build all possible cells within 3 transistors. Experimental results present three new multiplier structures with simulation results to show the creativity of our method.

This paper presents a method of design automation for analog circuits, focusing on topology generation and quick performance evaluation. First we describe mechanisms to generate circuit topologies with hierarchical blocks. Those blocks are specialized by adding terminal information. The connection between blocks is in compliance with a set of synthesis rules, which are extracted from typical schematics in the literature. Symbolic analysis has been used to select an appropriate topology quickly and to help the designer gain a better understanding of a circuit's behavior. Finally, experimental results show the creativity and efficiency of our method

This paper presents a method of design automation for analog circuits, focusing on topology generation and quick performance evaluation. First we describe a new mechanism to generate circuit topologies with hierarchical blocks, which are specialized by additional terminal information. The connection between blocks is in compliance with a set of synthesis rules, which are extracted from typical schematics in the literature. Fast symbolic analysis of linear performances is used to select appropriate topologies quickly. Finally, the selected topologies can be sized by an external sizing tool. Experimental results show the creativity and efficiency of our method

We present an extended method of automatic behavioral model generation for nonlinear analog circuits. The focus is on a decrease of simulation time. A procedural model formulation approach is introduced, together with a new simplification method based on the recognition of physical transistor properties of the element models. The simplification process is performed with respect to simulation time, and a hierarchical modeling approach is proposed. The result of these extensions are models with an obvious speed-up in simulation time compared to the simulation of the original netlists.

In this contribution we present the first method for model checking on nonlinear analog systems. Based on digital CTL model checking algorithms and results in hybrid model checking, we have developed a concept to adapt these ideas to analog systems. Using an automatic state space subdivision method the continuous state space is transfered into a discrete model. In doing this, the most challenging task is to retain the essential nonlinear behavior of the analog system. To describe analog specification properties, an extension to the CTL language is needed. Two small examples show the properties and advantages of this new method and the capability of the implemented prototype tool.

We present the first approach to model checking for nonlinear analog systems. Based on digital CTL model checking ideas, results in hybrid model checking and special needs in analog verification, a new model checking tool has been implemented Published model checking tools for hybrid systems require discrete or partly linear system descriptions. Our focus is on nonlinear analog behavior, therefore a new approach is necessary. There are mainly two aspects to be considered. Firstly, a discrete model retaining the essential nonlinear analog behavior has to be developed Secondly, model checking for analog systems requires extensions of the language to define analog system properties in a reasonable way.

In this paper we introduce an approach for parameter controlled symbolic analysis of nonlinear analog circuits. Based on a state-of-the-art algorithm, it enables the removal of specific circuit parameters from a symbolic circuit description, given as a set of nonlinear differential algebraic equations (DAEs). During the removal, singularities are considered, which includes structural changes of the set of DAEs. The feasibility of our approach is shown by several circuit examples.

We present a novel approach to optimization-based variation-tolerant analog circuit sizing. Using formal methods based on affine arithmetic, we calculate guaranteed bounds on the worst-case behavior and deterministically find the global optimum of the sizing problem by means of branch-and-bound optimization. To solve the nonlinear circuit equations with parameter variations, we define a novel affine-arithmetic Newton operator that gives a significant improvement in computational efficiency over an implementation using interval arithmetic. The calculation of guaranteed worst-case bounds and the global optimization are demonstrated by a prototype implementation.

We present a new methodology for current driven routing and layout verification for analog applications used to avoid defects due to electromigration.

This paper presents an approach to formal verification of linear analog circuits with parameter tolerances. The method proves that an actual circuit fulfils a specification in a given frequency interval for all parameter variations. It is based on a curvature driven bound computation for value sets using interval arithmetic. Some examples demonstrate the feasibility of this approach.

A fully automatic method for generating behavioral models for nonlinear analog circuits is presented. This method is based on simplifications of the system of nonlinear differential equations which is derived from a transistor level netlist. Generated models include nonlinear dynamic behavior. They are composed of symbolic equations comprising circuit parameters. Accuracy and simulation speed-up are shown by several examples.

This paper presents an approach to nonlinear dynamic analog circuit verification. The input-output behavior of two systems is analyzed to check whether they are functionally similar. The algorithm compares the implicit nonlinear state space descriptions of the two systems on the same or on different levels of abstraction by sampling the state spaces and by building a nonlinear one-to-one mapping of the state spaces. Some examples demonstrate the feasibility of our approach.