Abstract
Asynchronous circuit design can probably avoid the occurrence of various problems which arise in designing large synchronous circuits, such as clock skews and high power consumption. On the other hand, the cost of the verification of asynchronous circuits is usually much higher than that of synchronous circuits. This is because every change of wires should be taken into account in order to capture the behavior of asynchronous circuits unlike in the case of synchronous circuits. Furthermore, asynchronous circuit designers have recently preferred to use timed circuits for implementing fast and compact circuits. This trend increases the cost of verification, and at the same time increases the demands for formal verification tools. VINAS-P is our newest formal verification tool for timed asynchronous circuits using the techniques proposed in [1].The main idea in these techniques is the partial order reduction based on the timed version [2] of the Stubborn set method [3].
Chapter PDF
References
Yoneda, T., Ryu, H.: Timed trace theoretic verification using partial order reduction. In: Proc. of Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 108–121 (1999)
Yoneda, T., Schlingloff, H.: Efficient verification of parallel real-time systems. Formal Method in System Design, 187–215 (1997)
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed- Independent Circuits. MIT Press, Cambridge (1988)
Yoneda, T.: Verification of abstracted instruction cache of titac2. In: VLSI: Systems on a chip, pp. 373–384. Kluwer Academic Publishers, Dordrecht (1999)
Belluomini, W., Myers, C.: Verification of timed systems using POSETs. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 403–415. Springer, Heidelberg (1998)
Oikawa, K., Kitamura, K., Yoneda, T.: Saving memory for verification of asyn- chronous circuits. IEICE Technical Report (in Japanese) FTS99(11) 37–44 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoneda, T. (2000). VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_47
Download citation
DOI: https://doi.org/10.1007/10722167_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive