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. 1. Introduction Analog/mixed-signal (AMS) systems are a crucial part of today’s embedded systems. Typical AMS components such as sensors, transceivers, and signal conditioning enable interaction of embedded HW/SW systems with its physical environment. In today’s embedded systems, the functionality of the analog components is tightly interwoven with the digital HW/SW system. A particular challenge of AMS systems is that parameters cannot be assumed to be fixed to a deterministic value like in a digital system. Behavior of AMS systems cannot be assumed to be fixed for the following reasons: variations of parameters due to variations in the manufacturing process, but as well during operation (e.g., different temperatures, aging, and supply voltage) introduce deviations compared to an ideal reference. (Modeling) uncertainties are introduced by the fact that all models represent more or less accurate abstractions of physical reality. No model can be assumed to be absolutely accurate. Furthermore, computation with fixed-point arithmetic in the digital domain can contribute significantly to deviation from expected ideal behavior (rounding errors, quantization). In the following we refer to such deviations of a simulation run from possible real behavior in general as “deviations.” A communication system with typical variations and deviations is shown in Figure 1 as an example. Variations of gain, offset, or due to temperature (Figure 1, left) are compensated in software. This is done at lower layers of the software by controlling variable gain amplifier (VGA), voltage controlled oscillator (VCO). Higher layers of the software stack introduce further error correction mechanisms in software. Dependability of the overall system is defined by complex interaction of AMS parts with the software stack. While known statistical methods (e.g., Monte Carlo simulation) allow us computing other statistic properties like Bit or Packet Error Rates (BER, PER), open issues are questions such
References
[1]
R. Y. Rubinstein, Simulation and the Monte Carlo Method, John Wiley & Sons, New York, NY, USA, 1981.
[2]
D. E. Hocevar, M. R. Lightner, and T. N. Trick, “Study of variance reduction techniques for estimating circuit yields,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 2, no. 3, pp. 180–192, 1983.
[3]
K. Antreich, H. Gr？b, and C. Wieser, “Practical methods for worst-case and yield analysis of analog integrated circuits,” International Journal of High Speed Electronics and Systems, vol. 4, no. 3, pp. 261–282, 1993.
[4]
M. Rafaila, C. Grimm, C. Decker, and G. Pelz, “Sequential design of experiments for effective model-based validation of electronic control units,” e&i Elektrotechnik Und Informationstechnik, vol. 127, pp. 164–170, 2010.
[5]
M. S. Branicky, M. M. Curtiss, J. A. Levine, and S. B. Morgan, “RRTs for nonlinear, discrete, and hybrid planning and control,” in Proceedings of the 42nd IEEE Conference on Decision and Control, pp. 657–663, December 2003.
[6]
A. Bhatia and E. Frazzoli, “Incremental search methods for reachability analysis of continuous and hybrid systems,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '04), vol. 2993 of Lecture Notes in Computer Science, pp. 142–156, Springer, 2004.
[7]
A. Julius, G. Fainekos, M. Anand, I. Lee, and G. Pappas, “Robust test generation and coverage for hybrid systems,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '07), vol. 4416 of Lecture Notes in Computer Science, pp. 329–342, Springer, 2007.
[8]
J. M. Esposito, “Randomized test case generation for hybrid systems: metric selection,” in Proceedings of the 36th Southeastern Symposium on System Theory, pp. 236–240, 2004.
[9]
Q. Zhao, B. H. Krogh, and P. Hubbard, “Generating test inputs for embedded control systems,” IEEE Control Systems Magazine, vol. 23, no. 4, pp. 49–57, 2003.
[10]
J. Kapinski, B. H. Krogh, O. Maler, and O. Stursberg, “On Systematic simulation of open continuous systems,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '03), vol. 2623 of Lecture Notes in Computer Science, pp. 283–297, Springer, 2003.
[11]
A. Girard and G. Pappas, “Verification using simulation,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '06), vol. 3927 of Lecture Notes in Computer Science, pp. 272–286, Springer, 2006.
[12]
A. Chutinan and B. H. Krogh, “Computing polyhedral approximations to flow pipes for dynamic systems,” in Proceedings of the 37th IEEE Conference on Decision and Control (CDC '98), pp. 2089–2094, December 1998.
[13]
A. B. Kurzhanski and P. Varaiya, “Ellipsoidal techniques for reachibility analysis,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '00), vol. 1790 of Lecture Notes in Computer Science, pp. 202–214, Springer, 2000.
[14]
S. Prajna and A. Jadbabaie, “Safety verification of hybrid systems using barrier certificates,” in Proceedings of the International Workshop Hybrid Systems: Computation and Control (HSCC '04), vol. 2993 of Lecture Notes in Computer Science, pp. 477–492, Springer, 2004.
[15]
E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, The MIT Press, 1999.
[16]
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 1020 states and beyond,” Information and Computation, vol. 98, no. 2, pp. 142–170, 1992.
[17]
E. Clarke, O. Grumberg, and D. Long, “Verification tools for finite-state concurrent systems,” in Proceedings of the Decade of Concurrency, Reflections and Perspectives, vol. 803 of Lecture Notes in Computer Science, pp. 124–175, Springer, 1994.
[18]
O. Maler and G. Batt, “Approximating continuous systems by timed automata,” in Proceedings of the 1st international workshop on Formal Methods in Systems Biology (FMSB '08), vol. 5054 of Lecture Notes in Computer Science, Springer, 2008.
[19]
O. Stursberg, S. Kowalewski, and S. Engell, “On the generation of timed discrete approximations for continuous systems,” Mathematical and Computer Modelling of Dynamical Systems, vol. 6, no. 1, pp. 51–70, 2000.
[20]
O. Stursberg, S. Kowalewski, and S. Engell, “Timed approximations of hybrid processes for controller verification,” in Proceedings of the 1st IFAC Conference on Analysis and Design of Hybrid Systems, pp. 289–295, 2003.
[21]
R. Alur, T. A. Henzinger, G. Lafferriere, and G. J. Pappas, “Discrete abstractions of hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7, pp. 971–984, 2000.
[22]
T. Henzinger and H. Wong-Toi, “Linear phase-portrait approximations for nonlinear hybrid systems,” in Proceedings of the Hybrid Systems III: Verification and Control, vol. 1066 of Lecture Notes in Computer Science, pp. 377–388, Springer, 1996.
[23]
W. Hartong, L. Hedrich, and E. Barke, “Model checking algorithms for analog verification,” in Proceedings of the 39th Annual Design Automation Conference (DAC '02), pp. 542–547, June 2002.
[24]
D. Grabowski, D. Platte, L. Hedrich, and E. Barke, “Time constrained verification of analog circuits using model-checking algorithms,” Electronic Notes in Theoretical Computer Science, vol. 153, no. 3, pp. 37–52, 2006.
[25]
W. Hartong, L. Hedrich, and E. Barke, “On discrete modelling and model checking of nonlinear analog systems,” in Proceedings of the 14th International Conference on Computer Aided Verification (CAV ’02), pp. 401–413, 2002.
[26]
S. L？mmermann, A. Jesser, M. Rathgeber et al., “Checking heterogeneous signal characteristics applying assertion-based verification,” in Proceedings of the Frontiers in Analog Circuit Verification (FAC '09), Grenoble, France, 2009.
[27]
A. Pnueli and O. Maler, “Extending PSL for analog circuits,” Tech. Rep., 2005, PROSYD Deliverable D 1.3/1.
[28]
W. Heupke, C. Grimm, and K. Waldschmidt, “Semi-symbolic simulation of nonlinear systems,” in Proceedings of the Forum on Specification and Design Languages (FDL '05), ECSI, Lausanne, Switzerland, September 2005.
[29]
C. Grimm, W. Heupke, and K. Waldschmidt, “Refinement of mixed-signal systems with affine arithmetic,” in Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE '04), pp. 372–377, IEEE Press, February 2004.
[30]
C. Grimm, W. Heupke, and K. Waldschmidt, “Analysis of mixed-signal systems with affine arithmetic,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 1, pp. 118–123, 2005.
[31]
D. Grabowski, M. Olbrich, C. Grimm, and E. Barke, “Range arithmetics to speed up reachability analysis of analog systems,” in Proceedings of the Forum on Specification, Verification and Design Languages (FDL '07), Barcelona, Spain, 2007.
[32]
N. Femia and G. Spagnuolo, “True worst-case circuit tolerance analysis using genetic algorithms and affine arithmetic,” IEEE Transactions on Circuits and Systems, vol. 47, no. 9, pp. 1285–1296, 2000.
[33]
A. Lemke, L. Hedrich, and E. Barke, “Analog circuit sizing based on formal methods using affine arithmetic,” in Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD '02), pp. 486–489, November 2002.
[34]
C. F. Fang, R. A. Rutenbar, M. Püschel, and T. Chen, “Toward efficient static analysis of finite-precision effects in DSP applications via affine arithmetic modeling,” in Proceedings of the 40th Design Automation Conference (DAC '03), pp. 496–501, June 2003.
[35]
C. F. Fang, T. Chen, and R. A. Rutenbar, “Floating-point error analysis based on affine arithmetic,” in Proceedings of IEEE International Conference on Accoustics, Speech, and Signal Processing (ICASSP ’03), vol. 2, pp. 561–564, April 2003.
[36]
R. E. Moore, Interval Analysis, Prentice-Hall, Englewood Cliffs, NJ, USA, 1966.
[37]
D. Grabowski, M. Olbrich, and E. Barke, “Analog circuit simulation using range arithmetics,” in Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC '08), pp. 762–767, IEEE Computer Society Press, Seoul, Korea, March 2008.
[38]
K. J. ？str？m and T. H？gglund, PID Controllers: Theory, Design and Tuning, Instrument Society of America, 2nd edition, 1995.
[39]
D. Ryder-Cook, “Thermal modelling of buildings,” Tech. Rep., University of Cambridge, 2009.
