随着信息技术产业的高速发展,数字系统和集成电路已经在不知不觉中成为我们生活的一部分。第三方来源的IP核在集成电路中的广泛使用,使得信息系统内部及各种系统之间在数据交互时存在潜在的安全威胁。对于数据机密性、完整性要求较高的集成电路来说,需要确定IP核对系统关键数据的访问权限和修改权限,以保证IP核的使用不会造成关键数据的泄露或修改。本文对电路内部的数据流进行标记,在不影响电路原有功能的前提下,追踪电路中数据流的流向,并使用模型检测技术对电路设计进行安全路径验证。模型检测技术作为一种基于完备地搜索有穷状态空间的验证方法,可以全自动地验证电路系统或软件设计是否能够满足期望的属性。本文对模型检测方法的基本理论和基本原理进行了分析,并阐述了Kripke结构和CTL*、CTL、LTL时态逻辑。模型检测的特点正好可以用在本文的污迹标记的安全路径验证中,而模型检测的应用离不开有效的模型检测器,本文选用NuSMV作为模型检测工具。NuSMV可以清晰明了地刻画复杂的有限状态系统。本文提出基于污迹追踪的安全路径验证方法,对门级Verilog电路设计进行数据流的标记来追踪数据的流向,形成可追踪的IP核代码。在数据流标记和追踪的方法方面,本文还详细解释了各种简单逻辑门和触发器添加污迹追踪标签的方法及其内部算法。最后,本文设计并实现了一个创新的工具链,并对该工具链的主要算法、数据结构的设计和转换程序的设计进行了详尽的说明,此工具链可以将门级Verilog代码自动转换为污迹标记的NuSMV验证代码,可以实现IP核验证代码的自动化生成,并依托这种模型检测工具最终实现具有IP核系统的安全路径验证,保障了复杂集成电路系统设计的安全和可信。