No Access

SYMBOLIC REACHABILITY ANALYSIS FOR MULTIPLE-CLOCK SYSTEM DESIGN

JU-HWAN YI

Department of EECS, KAIST, Kuseong-dong Yuseong-gu, Daejeon, 305-701, Korea

179-68 Seongbuk-dong, Seongbuk-gu, Seoul, Korea.

Search for more papers by this author

and

CHONG-MIN KYUNG

Department of EECS, KAIST, Kuseong-dong Yuseong-gu, Daejeon, 305-701, Korea

Search for more papers by this author

https://doi.org/10.1142/S0218126605002520Cited by:0 (Source: Crossref)

Abstract

This paper proposes a symbolic reachability analysis method for multiple-clock system design, which is the first approach to deal with both synchronization problems caused by metastability and rate mismatch problems caused by clock frequency mismatches in a single framework. Three methods are described to reproduce problems that occur with multiple-clock system design during reachability analysis: (1) alternate evaluation for a system with two clocks as the base-line model, (2) nondeterministic delayed evaluation to reproduce a synchronization problem, and (3) double evaluation to reproduce a clock frequency mismatch. Experimental results on ISCAS 89 benchmark show an improvement factor of average CPU time as compared to Clarke's method by 1.29, 55.41, 2.19 and 45.23 times when alternate evaluation, double evaluation, alternate evaluation with NDDE and double evaluation with NDDE is applied, respectively.

Keywords:

References

K. Yorav, S. Katz and R. Kiper, Correct Hardware Design and Verification Methods (Springer, 2001) pp. 98–103. Crossref, Google Scholar
C. K.-K. Kwok, V. V. Gupta and T. Ly, Using assertion-based verification to verify clock domain crossing signals, Design & Verification Conf. (2003) . Google Scholar
E. M. Clarke, D. Kroening and K. Yorav, Specifying and verifying systems with multiple clocks, IEEE Int. Conf. Computer Design (2003), pp. 48–55 . Google Scholar
T. Ly, N. Hand and C. K.-K. Kwok, Formally verifying clock domain crossing jitter using assertion-based verification, Design & Verification Conf. (2004) . Google Scholar
The VIS Group, VIS: Verification interacting with synthesis, http://www-cad.eecs.berkeley.edu/Respep/Research/vis (1995) . Google Scholar
F. Brglez, D. Bryan and K. Kozminski, Combinational profiles of sequential benchmark circuits, IEEE Int. Symp. Circuits System (1989), pp. 1929–1934 . Google Scholar
R. E. Bryant, IEEE Trans. Comput. 35, 677 (1986). Web of Science, Google Scholar