Abstract
This paper presents a new approach for verification of asynchronous circuits by using automatic abstraction. It attacks the state explosion problem by avoiding the generation of a flat state space for the whole design. Instead, it breaks the design into blocks and conducts verification on each of them. Using this approach, the speed of verification improves dramatically.
Chapter PDF
Similar content being viewed by others
References
R. Alur and R. P. Kurshan. Timing analysis in cospan. In Hybrid Systems III. Springer-Verlag, 1996.
Peter A. Beerel, Teresa H.-Y. Meng, and Jerry Burch. Efficient verification of determinate speed-independent circuits. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 261–267. IEEE Computer Society Press, November 1993.
W. Belluomini, C. J. Myers, and H. P. Hofstee. Verification of delayed-reset domino circuits using ATACS. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 3–12, April 1999.
W. Belluomini and C.J. Myers. Verification of timed systems using posets. In International Conference on Computer Aided Verification. Springer-Verlag, 1998.
G. Berthelot. Checking properties of nets using transformations. In Lecture Notes in Computer Science, 222, pages 19–40, 1986.
R. K. Brayton. Vis: A system for verification and synthesis. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 428–432, 1996.
J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. PhD thesis, Carnegie Mellon University, 1992.
David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1989.
M. R. Greenstreet. Stari: Skew tolerant communication. unpublished manuscript, 1997.
J. Gu and R. Puri. Asynchronous circuit synthesis with boolean satisfiability. In IEEE Trans. CAD, Vol. 14No.8, pages 961–973, 1995.
H. P. Hofstee, S. H. Dhong, D. Meltzer, K. J. Nowka, J. A. Silberman, J. L. Burns, S. D. Posluszny, and O. Takahashi. Designing for a gigahertz. IEEE MICRO, May–June 1998.
R. Johnsonbaugh and T. Murata. Additional methods for reduction and expansion of marked graphs. In IEEE TCAS, vol. CAS-28no.1, pages 1009–1014, 1981.
Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor Varshavsky. Concurrent Hardware: The Theory and Practice of Self-Timed Design. Series in Parallel Computing. John Wiley & Sons, 1994.
E. Mercer, C. Myers, and Tomohiro Yoneda. Improved poset timing analysis in timed petri nets. Technical report, University of Utah, 2001. http://www.async.utah.edu.
Charles E. Molnar, Ian W. Jones, Bill Coates, and Jon Lexau. A FIFO ring oscillator performance experiment. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 279–289. IEEE Computer Society Press, April 1997.
D. Moundanos, J. Abraham, and Y. Hoskote. Abstraction techniques for validation coverage analysis and test generation. IEEE TC, 47(1):2–14, 1998.
T. Murata. Petri nets: Properties, analysis, and applications. In Proceedings of the IEEE 77(4), pages 541–580, 1989.
T. Murata and J. Y. Koh. Reduction and expansion of lived and safe marked graphs. In IEEE TCAS, vol. CAS-27,no. 10, pages 68–70, 1980.
C. Ramchandani. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets. PhD thesis, MIT, Feb. 1974.
R. Alur R. Grosu and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In 12th International Conference on Computer-Aided Verification, LNCS 1855, pages 280–295, 2000.
Oriol Roig. Formal Verification and Testing of Asynchronous Circuits. PhD thesis, Univsitat Politècnia de Catalunya, May 1997.
Shai Rotem, Ken Stevens, Ran Ginosar, Peter Beerel, Chris Myers, Kenneth Yun, Rakefet Kol, Charles Dike, Marly Roncken, and Boris Agapiev. RAPPID: An asynchronous instruction length decoder. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 60–70, April 1999.
I. Suzuki and T. Murata. Stepwise refinements for transitions and places. New York: Springer-Verlag, 1982.
I. Suzuki and T. Murata. A method for stepwise refinements and abstractions of petri nets. In Journal Of Computer System Science, 27(1), pages 51–76, 1983.
S. Tasiran, R. Alur, R. Kurshan, and R. Brayton. Verifying abstractions of timed systems. In LNCS, volume 1119, pages 546–562. Springer-Verlag, 1996.
S. Tasiran and R. K. Brayton. Stari: A case study in compositional and heirarchical timing verification. In Proc. International Conference on Computer Aided Verification, 1997.
Tomohiro Yoneda and Hiroshi Ryu. Timed trace theoretic verification using partial order reduction. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 108–121, April 1999.
Hao Zheng. Specification and compilation of timed systems. Master’s thesis, University of Utah, 1998.
Hao Zheng. Automatic Abstraction for Synthesis and Verification of Timed Systems. PhD thesis, University of Utah, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zheng, H., Mercer, E., Myers, C. (2001). Automatic Abstraction for Verification of Timed Circuits and Systems?. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_16
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive
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.
