Model Checking on Clock Domain Crossing Design of System-on-Chip
Xu Cheng · Dianzi xuebao · 2008
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.