Formal verification of mixed-signal designs using extended affine arithmetic

2016 ◽  
Author(s):  
Carna Radojicic ◽  
Christoph Grimm
Keyword(s):  
Formal Verification ◽  
Affine Arithmetic ◽  
Mixed Signal

scholarly journals Verification of Mixed-Signal Systems with Affine Arithmetic Assertions

VLSI Design ◽  
2013 ◽  
Vol 2013 ◽  
pp. 1-14 ◽  
Author(s):  
Carna Radojicic ◽  
Christoph Grimm ◽  
Florian Schupfer ◽  
Michael Rathmair
Keyword(s):  
Embedded Systems ◽  
Affine Arithmetic ◽  
Small Deviations ◽  
Mixed Signal ◽  
Signal Systems ◽  
System Properties ◽  
Formal Techniques

Embedded systems include an increasing share of analog/mixed-signal components that are tightly interwoven with functionality of digital HW/SW systems. A challenge for verification is that even small deviations in analog components can lead to significant changes in system properties. In this paper we propose the combination of range-based, semisymbolic simulation with assertion checking. We show that this approach combines advantages, but as well some limitations, of multirun simulations with formal techniques. The efficiency of the proposed method is demonstrated by several examples.

ANALOG/MIXED-SIGNAL CIRCUIT VERIFICATION USING MODELS GENERATED FROM SIMULATION TRACES

2010 ◽  
Vol 21 (02) ◽  
pp. 191-210 ◽  
Author(s):  
SCOTT LITTLE ◽  
DAVID WALTER ◽  
KEVIN JONES ◽  
CHRIS MYERS ◽  
ALPER SEN
Keyword(s):  
Formal Verification ◽  
Phase Detector ◽  
System Level ◽  
Switched Capacitor ◽  
Levels Of Abstraction ◽  
Mixed Signal ◽  
Circuit Verification ◽  
System Level Simulation

Verification of analog/mixed-signal (AMS) circuits is complicated by the difficulty of obtaining circuit models at suitable levels of abstraction. We propose a method to automatically generate abstract models suitable for formal verification and system-level simulation from transistor-level simulation traces. This paper discusses the application of the proposed methodology to a switched capacitor integrator and PLL phase detector.

scholarly journals Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis

10.29007/x211 ◽  
2018 ◽  
Author(s):  
Omar Beg ◽  
Ali Davoudi ◽  
Taylor T Johnson
Keyword(s):  
Formal Verification ◽  
Charge Pump ◽  
Phase Locked Loop ◽  
Reachability Analysis ◽  
Phase Locked Loops ◽  
Hybrid Automata ◽  
Mixed Signal ◽  
Full Wave ◽  
Mission Critical ◽  
A Charge

Analog-mixed signal (AMS) circuits are widely used in various mission-critical applications necessitating their formal verification prior to implementation. We consider modeling two AMS circuits as hybrid automata, particularly a charge pump phase-locked loop (CP-PLL) and a full-wave rectifier (FWR). We present executable models for the benchmarks in SpaceEx format, perform reachability analysis, and demonstrate their automatic conversion to MathWorks Simulink/Stateflow (SLSF) format using the HyST tool. Moreover, as a next step towards implementation, we present the VHDL-AMS description of a circuit based on the verified model.

Sign in / Sign up

Export Citation Format

Share Document