3.3.1 等价性检查(EC) 等价性检查(Equivalence Checking,EC)不是形式验证皇冠上的那颗最耀眼的钻石——模型检测(Model Checking)常以直观的状态空间探索吸引初学者,定理证明(Theorem Proving)则以数学的庄严感俘获理论派;但若你曾在凌晨三点盯着综合后网表与RTL行为不一致的波形抓耳挠腮,若你曾因一次未被覆盖的复位释放路径导致芯片回片后功能异常而彻夜难眠,若你曾在签核前最后一刻发现时序驱动综合工具悄悄重写了关键控制逻辑——那么你会明白:等价性检查,是数字电路可信交付链条中那根绷得最紧、也最不容松动的钢索。 它不许诺“系统永远安全”,也不承诺“所有输入都已穷尽”;