Article

Model checking of S3C2400X industrial embedded SOC product

Authors:

Hoon Choi,

Byeongwhee Yun,

Yuntae Lee,

Hyunglae RohAuthors Info & Claims

DAC '01: Proceedings of the 38th annual Design Automation Conference

Pages 611 - 616

https://doi.org/10.1145/378239.379034

Published: 22 June 2001 Publication History

Get Access

Abstract

This paper describes our experience and methodology used in the model checking of S3C2400X industrial embedded SOC product. We employed model checking to verify the RTL implementation. We describe how to model the multiple clocks, gated clocks, unsynchronized clocks, and synchronization logics in model checking. Detailed case studies of real designs show the application of the proposed modeling techniques, environment modeling, and the properties we checked. The verification results validate the proposed techniques by finding real bugs.

References

[1]

K. L. McMillan, Cadence SMV, available at http://wwwcad.eecs.berkeley.edu/kenmcmil.

Google Scholar

[2]

B. Chen, M. Yamazaki, and M. Fujita, "Bug Identification of a Real Chip Design by Symbolic Model Checking," in ED&TC, pp. 132-136, 1994.

Google Scholar

[3]

J. Bormann, J. Lohse, M. Payer, and G. Venzl, "Model Checking in Industrial Hardware Design," in 32nd DAC, pp. 298-303, 1995.

Digital Library

Google Scholar

[4]

J. Lu, S. Tahar, D. Voicu, and X. Song, "Model Checking of a Real ATM Switch," in ICCD, pp. 195-198, 1998.

Digital Library

Google Scholar

[5]

A. Th. Eiriksson, "Integrating Formal Verification Methods with A Conventional Project Design Flow," in 33rd DAC, pp. 666-671, 1996.

Digital Library

Google Scholar

[6]

K. Takayama, T. Satoh, T. Nakata, and F. Hirose, "An Approach to Verify a Large Scale System-on-a-chip Using Symbolic Model Checking," in ICCD, pp. 308-313, 1998.

Digital Library

Google Scholar

[7]

H. Choi, M.K. Yim, J.Y. Lee, B.W. Yun, and Y.T. Lee, "Formal Verification of an Industrial System-on-a-chip," in ICCD, pp. 453-458, 2000.

Digital Library

Google Scholar

[8]

AMBA Specification manual, England: ARM, 1999.

Google Scholar

[9]

USB Host Controller User's Manual, Phoenix Tech., 1999.

Google Scholar

Recommendations

Model Checking on Product Structures
FMCAD '98: Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design

We present an algorithm for checking CTL formulas in Kripke structures with side conditions, where the side conditions define new variables in terms of path formulas. Given any CTL formula where the defined variables may occur, the presented algorithm ...
Model Checking CTL*[DC]
TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

We define a logic called CTL*[DC] which extends CTL* with ability to specify past-time and quantitative timing properties using the formulae of Quantified Discrete-time Duration Calculus (QDDC). Alternately, we can consider CTL*[DC] as extending logic ...
Symbolic model checking of software product lines
ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2ⁿ individual systems to verify. As each individual ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '01: Proceedings of the 38th annual Design Automation Conference

June 2001

863 pages

ISBN:1581132972

DOI:10.1145/378239

Chairman:
Jan Rabaey
Univ. of California

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 June 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DAC01

Sponsor:

EDAC
SIGDA
IEEE-CAS

DAC01: 38th ACM/IEEE-CAS/ EDAC Design Automation Conference

Nevada, Las Vegas, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
16
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Index Terms

Recommendations

Model Checking on Product Structures

Model Checking CTL*[DC]

Symbolic model checking of software product lines