Notes
概念卡片、推导草稿与速查。
用伪 Lean 风格记录一条两级流水线「气泡与有效位」不变量的证明草稿，供后续机械化。
阅读 ABC / 相关论文后对 AIG 局部重写目标、收益度量与验证闭环的整理。
布尔可满足性 vs 带理论的可满足性——形式化验证里最常碰到的两把钥匙。
逻辑综合与化简时常用的几条代数律，做成可检索卡片。