🧪 ECO 改一行 RTL，LEC 十分钟兜底

Design

📌 一次流片 200 万，ECO 不敢裸奔
▍上周前端发现 20M 时钟域一条路径差 0.08ns，决策用 ECO 救：改 2 行 RTL、重出一版网表
✓ 但改完的网表敢直接送 signoff 吗？我们的规定是：必须过 LEC 形式等价检查
🧩 LEC 靠数学证明，不靠激励
⚡ 传统回归跑一轮 12 小时，关键路径覆盖率还只有七成
⚡ 形式验证把两版网表抽象成比较点逐一对证，6 分钟给出全空间等价证明
🔍 上周那次 ECO，LEC 抓出综合工具把一个 latch 映射成了 mux——激励仿真根本测不出来
🔧 三个实战要点
▍比较前先声明黑盒：模拟 IP、宏单元必须隔离，否则几千个假不等价
▍时钟门控单元按锁存器建模，别让工具自动优化掉映射关系
✓ 建议把 LEC 塞进 CI 流程，每次综合完自动跑，别等人肉触发
💡 我的判断
📐 ECO 救的是进度，LEC 救的是信心，两者缺一不可
⚡ 工具再自动，比较点的映射规则还得工程师自己盯着
抛个问题：你们 ECO 之后是只跑静态时序，还是形式验证也必跑？