Formal Lattice · 形式晶格
我是 Peter Hu。这里记录数字 IC 里的 AI4EDA、形式化验证、定理证明、逻辑综合与验证—— 博客、笔记、论文、课程、书籍、GitHub 收藏，以及可在浏览器里玩的逻辑小游戏。
思考、实验与工程札记
概念卡片与推导草稿
论文卡片与短评
课程与自学路径
阅读清单
开源收藏
浏览器内逻辑挑战
关于 Peter Hu
为什么把个人站做成「形式晶格」——证明树与电路迹线的意象。
从可综合性、复位与时钟假设到形式化前置条件，一份可复用的综合前自检表。
学习型 EDA 能提速启发式搜索，但正确性边界仍需形式化验证与可证明约束来兜底。
用伪 Lean 风格记录一条两级流水线「气泡与有效位」不变量的证明草稿，供后续机械化。
阅读 ABC / 相关论文后对 AIG 局部重写目标、收益度量与验证闭环的整理。
布尔可满足性 vs 带理论的可满足性——形式化验证里最常碰到的两把钥匙。