形式化驗證的硬件木馬檢測：從RTL到版圖的多層安全防護 摘要

隨著全球半導(dǎo)體供應(yīng)鏈復(fù)雜化，硬件木馬（Hardware Trojan）已成為威脅芯片安全的關(guān)鍵風(fēng)險。本文提出一種基于形式化驗證的多層硬件木馬檢測框架，覆蓋寄存器傳輸級（RTL）、門級網(wǎng)表（Gate-Level Netlist）及物理版圖（Layout）三個階段，通過屬性驗證、等價性檢查和電磁特征分析構(gòu)建縱深防御體系。實驗表明，該方法可檢測出尺寸小于0.01%的觸發(fā)式木馬，誤報率低于0.5%，且對設(shè)計周期影響小于15%。