本文的研究内容是作者在英飞凌硕士实习期间,参与完成的手机基带SOC(system on chip:即片上系统)项目验证内容的一部分。作者深入研究了形式验证在SOC设计中的具体应用。并结合由英飞凌所开发的形式验证工具ONESPIN,研究了形式验证在SOC设计中的流程和具体的实施方法。通过对形式验证流程的深入研究,作者提出了一种简化流程的方法。该方法具有很高的直观性和高效性。本文阐述了运用ONESPIN进行一致性检查和等价性检查的具体方法。研究了一个具体的设计在形式验证各阶段在工具内部的表现形式。同时引入了ONESPIN的一些常用命令。详细研究了形式验证中的模块验证,也叫做特征检查,阐述了模块验证的具体流程,并结合一个小的设计实例研究了如何编写特征例(Property),如何查找错误。同时引入了基于ONESPIN的特征语言ITL(Internal Language)。以SOC设计中至关重要的PCL(port control ligic:即端口控制逻辑)模块为实例,研究如何针对该模块开展特征检查,并编写特征例。针对在SoC的验证中如何简化特征检查流程、提高验证效率的问题,给出了一种切实可行的简化特征检查流程的方法,并详细介绍了运用这种简化流程的方法进行特征检查的图形界面。本论文研究的内容已经广泛的应用于SOC的验证中,论文中所提出的简化特征检查的策略也成功地运用到了实际工程项目中。工程实践表明,该方法能有效简化特征检查流程、提高验证效率,具有高效可靠直观等优点。