Abstract
This paper presents an approach to verifying that a circuit as described by a continuous, differential equation model is a correct implementation of a discrete specification. The abstraction from continuous trajectories to discrete traces is based on topological features of the continuous model rather than quantizing the continuous phase space. An practical verification method based on numerical integration is presented. The method is demonstrated by the verification that a toggle circuit satisfies a discrete specification.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. W. Brockett. Smooth dynamical systems which realize arithmetical and logical operations. In Hendrik Nijmeijer and Johannes M. Schumacher, editors, Three Decades of Mathematical Systems Theory: A Collection of Surveys at the Occasion of the 50th Birthday of J. C. Willems, volume 135 of Lecture Notes in Control and Information Sciences, pages 19–30. Springer-Verlag, 1989.
Mark R. Greenstreet and Peter Cahoon. How fast will the flip flop? In Proceedings of the 1994 International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 77–86, Salt Lake City, November 1994. IEEE Computer Society Press.
Lance A. Glasser and Daniel W. Dobberpuhl. The Design and Analysis of VLSI Circuits. Addison-Wesley, 1985.
Aarti Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1(2/3): 151–258, October 1992.
Thomas A. Henzinger and Pei-Hsin Ho. Algorithmic analysis of nonlinear hybrid systems. In Proceedings of CAV 95, pages 225–238, 1995.
R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symsbolic reduction. IEEE Transactions on Computer-Aided Design, 10(11):1356–1371, November 1991.
Leslie Lamport and Fred B. Schneider. The ‘Hoare logic’ of CSP, and all that. ACM Transactions on Programming Languages, 6(2), April 1984.
A. Olivero, J. Sifakis, and S. Yovine. Using abstractions for the verification of linear hybrid systems. In David L. Dill, editor, Proceedings of 1994 Workshop on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 81–94. Springer-Verlag, June 1994.
Thomas S. Parker and Leon O. Chua. Prectical Numerical Algorithms for Chaotic Systems. Springer-Verlag, New York, 1989.
William H. Press, Brian P. Flannery, et al. Numerical Recipes in C: The art of numerical computing. Cambridge University Press, 1988.
Jiren Yuan and Christer Svensson. High-speed CMOS circuit technique. IEEE Journal of Solid-State Circuits, 24(1):62–70, February 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Greenstreet, M.R. (1996). Verifying safety properties of differential equations. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_76
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_76
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive