-
形式化验证的硬件木马检测：从RTL到版图的多层安全防护 摘要
随着全球半导体供应链复杂化，硬件木马（Hardware Trojan）已成为威胁芯片安全的关键风险。本文提出一种基于形式化验证的多层硬件木马检测框架，覆盖寄存器传输级（RTL）、门级网表（Gate-Level Netlist）及物理版图（Layout）三个阶段，通过属性验证、等价性检查和电磁特征分析构建纵深防御体系。实验表明，该方法可检测出尺寸小于0.01%的触发式木马，误报率低于0.5%，且对设计周期影响小于15%。
随着全球半导体供应链复杂化，硬件木马（Hardware Trojan）已成为威胁芯片安全的关键风险。本文提出一种基于形式化验证的多层硬件木马检测框架，覆盖寄存器传输级（RTL）、门级网表（Gate-Level Netlist）及物理版图（Layout）三个阶段，通过属性验证、等价性检查和电磁特征分析构建纵深防御体系。实验表明，该方法可检测出尺寸小于0.01%的触发式木马，误报率低于0.5%，且对设计周期影响小于15%。
