Abstract
In this paper we demonstrate a potential extension of formal verification methodology in order to deal with time-domain properties of analog and mixed-signal circuits whose dynamic behavior is described by differential algebraic equations. To model and analyze such circuits under all possible input signals and all values of parameters, we build upon two techniques developed in the context of hybrid (discrete-continuous) control systems. First, we extend our algorithm for approximating sets of reachable sets for dense-time continuous systems to deal with differential algebraic equations (DAEs) and apply it to a biquad low-pass filter. To analyze more complex circuits, we resort to bounded horizon verification. We use optimal control techniques to check whether a Δ-Σ modulator, modeled as a discrete-time hybrid automaton, admits an input sequence of bounded length that drives it to saturation.
This work was partially supported by the European Community projects IST-2001-33520 CC (Control and Computation) and IST-2003-507219 PROSYD (Property-based System Design) and by the US Army Research Office (ARO) contract no. DAAD19-01-1-0485.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)
Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol. 2993. Springer, Heidelberg (2004)
Asarin, E., Dang, T.: Abstraction by projection. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 32–47. Springer, Heidelberg (2004)
Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20–35. Springer, Heidelberg (2003)
Asarin, E., Bournez, O., Dang, T., Maler, O.: Reachability analysis of piecewiselinear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)
Ascher, U.M., Petzold, L.R.: Stability of computational methods for constrained dynamics systems. SIAM Journal on Scientific Computing 14, 95–120 (1993)
Bemporad, A., Morari, M.: Control of systems integrating logic, dynamics, and constraints. Automatica 35, 407–427 (1999)
Brenan, K.E., Campell, S.L., Petzold, L.R.: Numerical Solution of Initial Value Problems in Ordinary Differential-Algebraic Equations. North Holland, Amsterdam (1989)
Chutinan, A., Krogh, B.H.: Verification of polyhedral invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 76–90. Springer, Heidelberg (1999)
Lubich, C., Hairer, E., Wanner, G.: Geometric Numerical Integration. In: Structure-Preserving Algorithms for Ordinary Differential Equations. Series in Comput. Mathematics, vol. 31. Springer, Heidelberg (2003)
Pérez-Verdú, B., Medeiro, F., Rodríguez-Vázquez, A.: Top-Down Design of High-Performance Sigma-Delta Modulators, ch. 2. Kluwer Academic Publishers, Dordrecht (2001)
Feldmann, U., Günther, M.: The DAE-index in electric circuit simulation. In: Proc. IMACS, Symposium on Mathematical Modelling, vol. 4, pp. 695–702 (1994)
Floberg, H.: Symbolic Analysis in Analog Integrated Circuit Design. Kluwer, Dordrecht (1997)
Ghosh, A., Verumi, R.: Formal verification of synthesized analog circuits. Int. Conf. on Computer Design 4, 40–45 (1999)
Goodson, M., Schreier, R., Zhang, B.: An algorithm for computing convex positively invariant sets for delta-sigma modulators. IEEE Transactions on Circuits and Systems I 44, 38–44 (1997)
Tomlin, C.J., Greenstreet, M.R. (eds.): HSCC 2002. LNCS, vol. 2289. Springer, Heidelberg (2002)
Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: Proc. ICCAD (2004) (to appear)
Hartong, W., Hedrich, L., Barke, E.: On discrete modelling and model checking for nonlinear analog systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 401–413. Springer, Heidelberg (2002)
Hein, S., Zakhor, A.: On the stability of sigma delta modulators. IEEE Transactions on Signal Processing 41 (1993)
Kouramas, K., Rakovic, S.V., Kerrigan, E.C., Mayne, D.Q.: Approximation of the minimal robustly positively invariant set for discrete-time LTI systems with persistent state disturbances. In: 42nd IEEE Conference on Decision and Control (2003)
Kurshan, R.P., McMillan, K.L.: Analysis of digital circuits through symbolic reduction. IEEE Trans. on Computer-Aided Design 10, 1350–1371 (1991)
Maler, O.: On optimal and sub-optimal control in the presence of adversaries. In: Workshop on Discrete Event Systems, (WODES) (2004) (to appear)
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proc. FORMATS/FTRTFT (2004) (to appear)
Maler, O., Pnueli, A. (eds.): HSCC 2003. LNCS, vol. 2623. Springer, Heidelberg (2003)
MOSEK ApS. The Mosek Optimization Toolbox for Matlab version 3.0 (revision 19) user’s guide and reference manual (November 2003)
Salem, A.: Semi-formal verification of VHDL-AMS descriptors. IEEE Int Symposium on Circuits and Systems 5, V-333–V336 (2002)
Schreier, R.: The delta-sigma toolbox version 6.0 (January 2003)
Sorensen, H.V., Aziz, P.M., Spiegel, J.V.D.: An overview of sigma-delta converters. IEEE Signal Processing Magazine, 61–84 (January 1996)
Varaiya, P.: Reach set computation using optimal control. In: Proc. KIT Workshop, Verimag, Grenoble (1998)
Wichmann, T.: Computer aided generation of approximate DAE systems for symbolic analog circuit design. In: Proc. Annual Meeting GAMM (2000)
Wichmann, T., Popp, R., Hartong, W., Hedrich, L.: On the simplification of nonlinear DAE systems in analog circuit design. In: Computer Algebra in Scientific Computing. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dang, T., Donzé, A., Maler, O. (2004). Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive