Automatic formal verification of clock domain crossing signals

ABSTRACT

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.

REFERENCES

• 1: T. Ly, C. K. Kwok, C. Widdoes., "A methodology for verifying sequential reconvergence of clock-domain crossing signals", Design and Verification Conference, 2005.
• 2: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 3: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 4: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 5: C. Cummings, "Synthesis and Scripting Techniques for Designing Multi-asynchronous Clock Designs," Synopsys Users Group (SNUG), 2001.
• 6: "Clock domain crossing-closing the loop on clock domain function implementation problems", 2004. Cadence Design Systems.
• 7: N. Hand, "The need for an automated clock domain crossing verification solution", Mentor Graphics Corporation, 2006.
• 8: S. Sarwary, S. Verma, "Critical clock-domain-crossing bugs", Electronics Design, Strategy, News, Apr. 3, 2008
• 9: T. Kapschitz, R. Ginosar, "Formal Verification of Synchronizers", Conference of Correct Hardware Design and Verification Methods, 2005.
• 10: C. Kwok, V. Gupta, T. Ly, "Using Assertion-based verification to verify clock domain crossing signals", Design and Verification Conference, 2003.
• 11: T. Kapschtiz, R. Ginosar, R. Newton, "Verifying Synchronization in Multi-Clock domain SoC", Design and Verification Conference, 2004.
• 12: "CheckWare Data Book--Assertion Library", Mentor Graphics Corporation.