随着集成电路制造技术和计算机技术的飞速发展，SoC设计已成为未来的发展趋势，而随着设计规模的扩大，设计验证也越来越成为制约其发展的瓶颈，其中功能验证更是该制约因素的重中之重。 SoC设计的规模要远远大于以往的IC设计，将SoC作为一个整体，并单纯采用传统的基于仿真向量的仿真技术很难保证快而有效得完成其验证；另外，SoC的一个很显著的特点就是广泛采用第三方IP，这使得买方无法进行白箱方式验证，明显得增加了SoC验证的难度。 针对上述问题，本文重点研究了SoC数字系统的验证方法。在分析了SoC数字系统设计验证的特点、形式验证技术的可行性及前人工作的基础上，将分级验证的思想应用到了SoC数字系统设计验证中，并采用了形式验证技术中比较成熟的模型检查方法对SoC数字系统的模块进行验证。在模块验证中，用Mealy模型替代Kripke模型对模块进行建模，达到了对模块的变量进行区分的目的，以此获的了模块间的关联信息。从而解决了对SoC数字系统的模块进行协调、高效验证的问题。同时，由于将系统划分成许多模块，并将系统的特性分散到系统级跟模块级的各个模块中，从而减小了验证的规模，降低了验证的难度，提高了验证的可靠性。 总之，本文在大量分析和研究的基础上，提出了适于SoC数字系统的验证方法，并对具体的实现技术进行了研究，为进一步解决SoC设计验证问题打下了基础。