Traditional approach in RTL verification cannot completely verify the clock domain crossing (CDC) design of SoC.To solve this problem

we first propose a RTL module to model the actual effect of metastability.Then

linear temporal logic is proposed to model the specification of CDC designs.To solve the exponential problem in model checking

based on the characteristic of CDC designs

a strategy on input signal partition for the state transition’s characteristic function and a strategy on induction are proposed.Experiment results demonstrate that our method is useful to find CDC errors in the RTL verification stage and the verification time is approximately reduced from exponential to polynomial increased with the register size.