Property generation method for model checking on Clock Domain Crossing design

Verification on Clock Domain Crossing (CDC) design is crucial to the SoC functional verification. Traditional model checking methods on CDC design do not consider the completeness of properties. However, generating complete design properties is the basis for model checking, and incomplete properties would lead to bug escape. To generate complete properties for CDC design, we first propose a finite state automaton based property generation method. Then, to solve the exponential explosive problem, we propose a metastability based data type reduction strategy. Experiment results on two typical CDC designs show that, our approach not only achieves 100% property coverage, but also discovers a bug that escaped by traditional methods. Meanwhile, the verification time for model checking is greatly reduced.EI02258-2653