在硬件,协议设计上巨大成功 ■现有手段:测试、仿真 太多可能、慢、无法穷尽、没有保障 o举例:加法器测试:2160个浮点数对 形式化方法 o自动证明、确定性结果 o奔4浮点数计算部牛刀小试: 2003: FV found many high-quality bugs in P4 and verified"20%of design FV is now standard practice in the floating-point domain o Can we do more? 2009: Replacing Testing with Formal Verification in Intel CoreTM Processor Execution Engine validation a CAV09在硬件，协议设计上巨大成功 ◼ 现有手段：测试、仿真  太多可能、慢、无法穷尽、没有保障  举例：加法器测试：2 160个浮点数对… ◼ 形式化方法  自动证明、确定性结果  奔4 浮点数计算部 牛刀小试：  Can we do more？ 2003：FV found many high-quality bugs in P4 and verified “20%” of design FV is now standard practice in the floating-point domain 2009：Replacing Testing with Formal Verification in Intel 𝐂𝐨𝐫𝐞𝐓𝐌 i7 Processor Execution Engine Validation @ CAV09