Towards Formal Verification Of Analog Designs: Smriti Gupta

Towards Formal Verification of Analog Designs Smriti Gupta Bruce Krogh Rob A. Rutenbar

[email protected] [email protected] [email protected]

Carnegie Mellon University Pittsburgh, PA • Research supported by the Semiconductor Research Corporation

1

Big Question: Can We Formally Verify Analog…?

DIGITAL

ANALOG

Analog Methodology  Simulation

Digital Methodology  Simulation  Abstraction  Formal verification

 Abstraction  Formal verification

2

Outline 

Background  Where does verification fit into analog design flow?



Hybrid System Verification  What is it? Why useful for analog?  Our hybrid checker: CheckMate  A small analog circuit example to illustrate ideas



A real circuit verification task: Delta Sigma Modulator  Overview of the delta sigma modulator  Bad behavior explained  Formal verification and analysis 3

Verification in the Analog Design Flow Develop systemreqs



Systemdesign &partition Idealizedblocks/cells Cell behavioral modeling

Circuitlevel design

Blocklevel design

Cell simulate

Block simulate

Sizedschematics Cell layout Cell parasitics for cell models Cell extract& backannotate Block&chip layout



Redesignif cells fail insystemintegration

Can we check early if there are problems with the spec or with the idealized initial design?

Cell parasitics for cell/block design Redesignif system integrationfails

Estimate chipparasitics Interconnectparasitics Realistic cell models Systemmodel for integration Fab&test

Initial verification problem



System integration verif. problem



Can we check late for problems caused when ideal blocks become real4

Verifying Analog Designs as Hybrid Systems 

Hybrid systems: Interacting discretecontinuous dynamics



Model checking for hybrid systems  construct a finite-state abstraction of the continuous dynamics





verify the abstraction reachability or ACTL specifications



if the verification is inconclusive, refine the abstraction

Application to Analog Circuits  continuous dynamics: differential or difference equations 5

CheckMate: Hybrid System Verification Tool 1. Constructs finite-state abstraction with transition relation based on polyhedral representations of q q' continuous flows p

p' π'1 π'2

Polyhedral sets of initial continuous states & parameters

π (π'1,p',q') (π,p,q) (π'2,p',q')

Specifications over discrete states 2. Applies model • Reachability checking to resulting • ACTL transition system. www.ece.cmu.edu/~webk/

3. Refines abstraction if necessary.

MATLAB/Simulink model

6

Computing Flowpipes for Continuous Dynamics Given a set of initial states, the procedure is to generate a sequence of polyhedra that contains all state trajectories (flows) from that set.  0 1 E.g. x&  0 0   1 2 Xo

0

Features of the  1 x  approach: 2 • each polyhedra : set of initial states

contains flows for ∆tk = tk+1 − tk • applies to nonlinear dynamics • includes piecewise constant inputs • approximation error 7 can be made arbitrarily

Illustration Circuit: Tunnel Diode Oscillator Verification question: For specified device parameters and ranges of initial states, will the circuit oscillate Start correctly? I here L

??? VC From: Walter Hartong, Lars Hedrich, and Erich Barke, “Model Checking Algorithms for Analog Verification.” Design Automation Conference, 2002, pp. 542-547.

8

Current(0-1e-3A)

Specification as a Finite-State Machine p7=currentis .7e-3

IL

p3=currentis .3e-3

Threshold 2 Threshold 1

VC

Voltage(0-0.5V)

IL

IL

Threshold 2

Threshold 2 Threshold 1

Threshold 1

VC

VC IL

Threshold 2 Threshold 1

Start IL

Threshold 2

VC

Threshold 1

VC

9

Current (0-1e3 A)

CheckMate Model

circuit dynamics

locati on3

p7 = current is .7e-3 locati p3 = current is on2 .3e-3 locati on1

Voltage (0-0.5V)

thresholds Checkmate Model

Finite State Machine

10

Flowpipes and Finite-State Abstractions

Non – Oscillating Case

Oscillating Case ­4

x 10

­4

locatio n3

8

3

Current (X2)

6 4

IC S

2

0

0

0.1

0.2

0.3

Voltage (X1)

0.4

9

4

8

locatio n2

6

1

Flowpipe Approximati on

2

10

locatio n1

0.5

7

5*10-4 4 3

IC S

2

1 0

1

Flowpipe Approximati on

2

0

locatio n3 locatio n2

3

Current (X2)

10

-4 *10 x 10

0.1

0.2

0.3

0.4

locatio n1 0.5

Voltage (X1)

11

Flowpipe Detail Oscillating Case



­4

x 10

8

x 10 4

3

Current (X2)

6 4

2

10

0

locatio n2

IC S

2 0

­4

locatio n3

10

0.1

0.3

 

CheckMate computes flowpipe approximations dynamically Flowpipes are conservative, ie,guaranteed to bound real dynamics

*10-4

1

Flowpipe Approximati on 0.2

Important points

0.4

locatio n1

0.5

Voltage (X1)

12

A Real Circuit: Delta Sigma A/D Converter Digital

fs

Anal og

fs/2

Encodin g

∆ΣModulato r

inpu Anti-aliasing t LPF

fd/2 Downsampl ing



Sampled Signal

NoiseShaping Filter H(z)

One-Bit Quantiz er Digital Encodin g

D/A Digital to Analog Converter

High Resolution



Digital Filter Decima tor

Digital Output

Delta Sigma Modulator  Samples input signal at a rate much higher than the Nyquist rate, and converts it into a high-rate, low-resolution digital signal.  Shapes the noise introduced by the quantizer such that the noise is attenuated in the signal band and amplified outside the signal band (at high frequencies). Decimator  Low pass filter removes the 13 noise from the high

∆Σ-Modulation: Closer Look Digital fs

Analog

fs/2

input

Encoding HighResolution

∆Σ-Modulator

Digital Output

fd/2

Anti-aliasingLPF

Digital Filter

Downsampling

Decimator

Quantizer Integrator Z-1

Error (e[n])

1-bit quantizer compares analog signal to a 0V ref, outputs +1 or -1

D/A

This is a chain of amplifiers #amplifiers = “order” of system 14

Analysis of Quantization: Noise is Shaped

Analog

fs/2

input

∆Σ-Modulator

Anti-aliasingLPF

HighResolution Digital Output

fd/2 Digital Filter

Downsampling

Decimator

fB

f re INPUT: Input signalq. spectrum

noise

fB

f re OUTPUT: Input signalq. and noise spectrum 15

∆Σ-Modulator: Undesired Behavior Means What? 



Instability



Quantizer Overload



Quantizer overload can cause the discrete-time integrators to hit saturation (max voltage limits).

If signal at the quantizer exceeds a specific maximum level—circuit no longer exhibits linear behavior

Quantizer Integrator

Error (e[n])

Z-1

D/A

16

Real Example: 3rd-Order ∆Σ Modulator Integrat or Quanti zer



Essential problem:

 A higher-order ∆Σ uses more amplifiers to 

better suppress noise But it also more unstable, more prone to

17

How Do We “Test” For Undesired Behavior? 3rd order ∆Σ Modulator

LPF

input +

noise

Criterion 1: Monitor the noise level • Low noise level in the signal band Criterion 2: Monitor the quantizer input • No overload: quantizer input should be between +/-2V 18

Criterion 1: Noise in Signal Band (LPF output) input Third-Order Delta Sigma Modulator

Input Signal

LPF

+

-

noise

DC Input

Noise Signal

Desired Low SNR

Undesire d High SNR

Time Samples

19

Criterion 2: Quantizer Overload

Quantizer Input

Undesire d Behavior

Desired Behavior

Time Samples 20

To Verify the ∆Σ Modulator 

Select a reasonable set of initial (continuous) states  Remember – this isn’t a digital circuit!  Need to start verification from some “sensible” known region of state space



Build a complete CheckMate model  Switched continuous dynamics for continuous circuits  FSM abstraction of high level behavior



Run CheckMate model  Check if undesired behaviors manifest as “bad” parts of state space reached 21

∆Σ Modulator: Selecting the Range of Initial States Random Input

Reached states (no overload)

selected set of initial states for verification state bounds

22

∆Σ Modulator: Building CheckMate Model NoiseShaping & LPF Filters

Quanti zer FSM

Hyperplanes defining various regions for the quantizer input “zero_threshold ”:x>0 “overload” : -2 <x<2

Hyperplane defining the desired region of the LPF

Low Pass Filter FSM 23

∆Σ Modulator: Modeling Quantizer as FSM

Hyperplane defining the desired region of the LPF 24

∆Σ Modulator: Modeling Quantizer as FSM

Quantizer states: current & previous quantizer output (inputs to noise-shaping & low-pass filters)

Hyperplane defining the desired region of the LPF 25

∆Σ Modulator: Modeling Quantizer as FSM "Avoid" state defines quantizer overload (reachability specification)

Hyperplane defining the desired region of the LPF 26

Result: CheckMate Reachability Computations Quantizer overload (first violations) (two views)

quantizer threshold

 

Breadth-first reachability (wrt discrete transitions) ~3 minutes to find first violation at depth

27

Results: Effect of Quantizer Switching projection onto X1-X3 plane

 

Reachable sets "split" when crossing quantizer threshold Leads to multiple branches in (brute-force) depth- 28

Summary 

Can we formulate a useful analog verification task as a hybrid systems model checking problem?  Yes  ∆Σ Modulator is, to best of our knowledge, largest nontrivial circuit to have any useful continuous property checked formally



…but still many practical limitations  We check at idealized block level, ie, system-level

 

analog, not transistors Model setup is still rather arduous Still limited to low-orders systems with relatively few state variables

29

Next Steps 

Formal specifications for analog designs  Identify mixed-signal specifications amenable to time-





domain characterization Create parameterized specification primitives for CheckMate implementation

CheckMate model checker for analog designs  Develop modeling guidelines  Implement abstraction methods (leverage CT CheckMate)  Heuristics for polyhedral over approximations to reduce computation time  Refinement strategies



Apply recent developments to increase efficiency

30