Courses
形式化方法自学课单（以公开课程材料为纲）
为何收录
补齐「会用工业形式化工具」到「能陈述并证明不变量」之间的理论缺口，服务数字 IC 验证与 AI4EDA 安全合入。
大纲要点
- 时序逻辑与模型检测基础（LTL/CTL 直觉）。
- SAT/SMT 编码：bit-vector、数组、增量求解。
- 定理证明器工作流：规范、引理、自动化战术。
- 硬件案例：简易流水线或总线协议。
收获与作业向
- 每周：一页笔记进
/notes，含「定义 / 例子 / 疑问」。 - 课程项目意向：把一段 RTL 属性写成 SVA，并尝试在证明器里陈述同一性质的抽象版。
推荐入口章节
- 模型检测：可达性与不变式。
- SMT：位向量算术与除法陷阱。
- 定理证明：先做小引理，再谈自动化。