01
缺陷定位概述
什么是形式化验证中的缺陷定位？为什么需要专门的定位方法？定位流程全景图。
全景入门
02
断言与反例分析
断言（Assertion）的本质、反例（Counterexample）的结构、如何从反例波形中提取关键信息。
断言波形
03
约束求解器与SAT
SAT/SMT求解器在定位中的作用、如何利用求解器进行最小化反例、核心算法（DPLL、CDCL）简介。
SATSMT
04
基于UNSAT核心的定位
什么是UNSAT核心？如何从不可满足的约束中提取最小冲突集？工具实践（Z3、MiniSAT）。
UNSATZ3
05
Delta Debugging
Delta Debugging算法原理、在反例简化中的应用、二分法与Delta Debugging的对比。
简化算法
06
模型与代码的映射
RTL代码与形式化模型之间的对应关系、如何将定位结果映射回源代码行、常见映射陷阱。
RTL映射
07
覆盖度分析
代码覆盖率、功能覆盖率、断言覆盖率在定位中的辅助作用、如何利用未覆盖点定位缺陷。
覆盖率分析
08
假设与约束的检查
环境约束（Assumption）错误导致的虚假反例、如何区分设计缺陷与环境缺陷、约束一致性检查。
假设约束
09
时序相关缺陷定位
建立时间/保持时间违例在形式化验证中的表现、时钟域交叉（CDC）问题的定位、时序断言（SVA）的调试。
时序CDC
10
数据通路缺陷定位
算术逻辑单元（ALU）错误、数据路径中的位宽不匹配、定点与浮点运算的验证。
数据通路ALU
11
控制通路缺陷定位
有限状态机（FSM）状态跳转错误、状态编码冲突、死锁与活锁的检测。
FSM死锁
12
总线协议与互联缺陷
AXI/AHB协议违例定位、总线仲裁错误、地址译码逻辑错误。
AXI总线
13
存储系统缺陷定位
内存读写冲突、缓存一致性协议错误、FIFO溢出与下溢。
存储FIFO
14
安全属性验证与定位
信息流安全、非干扰属性、侧信道漏洞的定位方法。
安全侧信道
15
等价性检查中的缺陷定位
组合等价性检查、时序等价性检查、如何定位不匹配点。
等价性EC
16
形式化验证工具链
主流工具（JasperGold、VC Formal、OneSpin）的定位功能对比、工具特定调试技巧。
工具JasperGold
17
调试脚本与自动化
Tcl/Python脚本在批量反例分析中的应用、自动化定位流水线设计。
脚本自动化
18
可视化与波形分析
VCD/FSDB波形查看技巧、如何标记关键信号、波形对比定位法。
波形VCD
19
团队协作与缺陷管理
缺陷报告模板、如何与设计工程师高效沟通、缺陷追踪系统集成。
协作管理
20
复杂SoC系统级定位
多模块交互缺陷、全局属性与局部属性的冲突、系统级反例的分解方法。
SoC系统级
21
随机仿真与形式化结合
动态仿真与形式化验证的互补、如何利用仿真seed复现缺陷、混合验证策略。
仿真混合
22
抽象与细化技术
抽象反例（Spurious Counterexample）的处理、细化（Refinement）策略、CEGAR循环。
抽象CEGAR
23
归纳与不变式挖掘
归纳法证明、如何从失败证明中提取反例、不变式自动挖掘辅助定位。
归纳不变式
24
形式化验证中的常见误区
过度约束、不完备建模、忽略初始状态、属性写错。
误区避坑
25
工业案例研究（一）
处理器验证中的缺陷定位、流水线冒险、乱序执行错误。
处理器案例
26
工业案例研究（二）
GPU验证中的缺陷定位、着色器核心错误、内存控制器问题。
GPU案例
27
工业案例研究（三）
AI加速器验证中的缺陷定位、脉动阵列配置错误、数据流控制错误。
AI加速器案例
28
前沿技术
机器学习辅助缺陷定位、图神经网络在反例分析中的应用、大语言模型在调试中的潜力。
MLGNN
29
课程总结与知识图谱
核心知识点回顾、常见定位模式总结、个人成长路径建议。
总结图谱
30
综合实战项目
从零开始定位一个真实设计缺陷、完整报告撰写、项目答辩准备。
实战项目