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.