片上系统(System-on-Chip,SoC)通常采用自顶向下的设计流程,根据高层级的设计规约探索设计空间后,设计将以虚拟原型的方式实现,同时硬件设备从寄存器传输级RTL模型进行逐层精化并综合直至布局布线最终流片。若物理设备的具体实现与设计规约不一致,那么在虚拟原型上开发的系统软件(如设备驱动程序)将难以与物理设备协同运行,这可能会导致严重的系统故障。此外,硬件物理设备若是在流片后被发现存在与原设计规约不一致的缺陷,则将会给厂商造成巨大的损失。因此,如何检测硬件设备的实现与设计规约的一致性是构建正确片上系统的关键问题。针对上述问题,本文以检测片上系统的高层级设计规约与低层级实现之间的一致性为研究目标,设计了规约驱动的片上系统一致性检测框架。具体来说,本文的主要研究内容和贡献如下:(1).基于SystemRDL语言,本文提出了形式化设备模型自动生成方法。本文结合硬件寄存器描述语言SystemRDL,扩展了其语法语义以支持寄存器行为逻辑描述,并提出了转换规则将扩展后SystemRDL描述的设计规约自动转换为一个可执行的形式化设备模型FDM。如此,本文即可将不可执行的高层级设计规约自动转换为一个可执行的形式化设备模型以应用于自动化一致性检测。(2).基于符号化执行,本文提出了规约驱动的片上系统一致性检测框架。通过使用内核分析框架Kprobes,本文实现了从虚拟原型或物理设备收集驱动程序请求以及设备状态。以形式化设备模型FDM作为设计的黄金参照模型,本文使用收集到的驱动程序请求序列在FDM上进行符号化执行,并比较由相同驱动程序请求触发的设备状态和FDM状态以检测高层级的FDM与低层级实现(例如虚拟原型和物理设备)之间的一致性。(3).基于变异测试,本文设计了测试用例生成与一致性检测充分性评价方法。为了优化和提升一致性检测的充分性和效率,本文设计了具有硬件特性的变异算子和除变异体约束(Mutant-KillingConstraint)的生成规则,使用除变异体约束对低层级设备实现的潜在缺陷建模,在FDM中自动插桩除变异体约束并引导设备请求的自动化生成。本文提出了协作式符号化执行机制,使用生成的设备请求激励设备并收集设备状态,通过符号化执行插桩后的FDM来检测FDM与低层级实现之间的一致性,同时采用测试覆盖准则评价片上系统一致性检测的充分性。本文使用两个工业级网卡的虚拟原型和物理设备作为实验对象,实验结果表明,结合自动生成的FDM模型,本文提出的规约驱动的片上系统一致性检测方法不仅能够更加有效地检测出虚拟原型和物理设备中存在的缺陷,而且能够对一致性检测的充分性做出评估。