Automatic Formal Verification of Clock Domain Crossing Signals

Bing Li; Chris Ka-Kei Kwok; IEEE

doi:10.1109/ASPDAC.2009.4796554

Back

Conference proceeding

Automatic Formal Verification of Clock Domain Crossing Signals

Bing Li, Chris Ka-Kei Kwok and IEEE

PROCEEDINGS OF THE ASP-DAC 2009: ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 2009, pp.654-659

Asia and South Pacific Design Automation Conference Proceedings

01/01/2009

DOI: https://doi.org/10.1109/ASPDAC.2009.4796554

Abstract

Computer Science

Computer Science, Hardware & Architecture

Engineering

Engineering, Electrical & Electronic

Science & Technology

Technology

In this paper, we present an approach that uses formal methods to verify Clock Domain Crossing (CDC) issues in a fully automatic way. First, we discuss various CDC schemes and the corresponding checks that need to be formally verified. Then we demonstrate how to synthesize them into assertion logic. After that a fully automatic, on-the-fly formal CDC approach is proposed. To the best of our knowledge, this is the first paper discussing fully automatic, on-the-fly formal verification of CDC signals. Experiment results show that our automatic formal CDC, when compared with the conventional post-CDC formal CDC, takes much less time, but still prove significant number of CDC checks.

Metrics

3 Record Views

See more details

Details

Title: Automatic Formal Verification of Clock Domain Crossing Signals
Creators - without role: Bing Li - Mentor
Chris Ka-Kei Kwok - Mentor
IEEE
Publication Details: PROCEEDINGS OF THE ASP-DAC 2009: ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 2009, pp.654-659
Series: Asia and South Pacific Design Automation Conference Proceedings
Publisher: IEEE
Number of pages: 6
Identifiers: 9941664108331
Academic Unit: King Abdullah University of Science & Technology
Language: English
Resource Type: Conference proceeding