第1章
形式化验证概述
什么是形式化验证 · 为什么需要 · 与动态仿真对比 · 应用场景
基础概念
第2章
形式化验证基础理论
布尔逻辑 · 命题/谓词逻辑 · 时序逻辑LTL/CTL · 模型检测
理论核心
第3章
形式化验证工具链
JasperGold · VC Formal · OneSpin · 选型 · 安装配置
工具环境
第4章
断言语言基础 (SVA)
SVA语法 · sequence/property · assert/cover · 形式化用法
SVA断言
第5章
形式化验证流程
需求分析 · 规格建模 · 属性提取 · 约束编写 · 验证计划
流程方法论
第6章
约束编写技巧
时钟/复位约束 · 输入/输出约束 · assume/guarantee · 完备性
约束进阶
第7章
属性 (Property) 编写
Safety/Liveness · 公平性 · 有界/无界 · 分解策略
属性核心
第8章
形式化验证中的抽象技术
抽象概念 · CEGAR · 数据路径抽象 · 控制逻辑抽象
抽象高级
第9章
形式化验证与UVM集成
UVM平台回顾 · 形式化角色 · 序列映射 · 混合验证
UVM集成
第10章
形式化验证中的覆盖率
代码/功能/形式化覆盖率 · 覆盖点 · 覆盖率驱动收敛
覆盖率度量
第11章
形式化验证调试技巧
反例分析 · 波形调试 · 属性/约束调试 · 工具使用
调试实战
第12章
等价性检查
组合/时序等价性 · 带状态等价性 · 应用场景
等价性检查
第13章
FPV 形式化属性验证
FPV概念 · 与仿真协同 · 验证计划 · 案例分析
FPV属性
第14章
Formal Apps 技术
什么是Apps · Connectivity/X-Prop/Unreachable · 使用流程
Apps效率
第15章
Datapath 验证
Datapath挑战 · 算术运算 · 乘法器/加法器 · 浮点验证
Datapath运算
第16章
Control Logic 验证
状态机 · 仲裁逻辑 · 握手协议 · 流水线控制
控制逻辑
第17章
Memory 验证
Memory模型 · 读写一致性 · 地址译码 · BIST验证
Memory存储
第18章
Interconnect 验证
AXI/ACE/CHI · 死锁/活锁检测 · 数据完整性
总线互联
第19章
Security 验证
安全属性 · 信息流分析 · 权限检查 · 侧信道分析
安全隐私
第20章
Low Power 验证
电源域 · 电压切换 · 隔离单元 · 电源管理状态机
低功耗电源
第21章
Reset 验证
复位序列 · 异步复位同步释放 · 域交叉 · 完整性
复位时序
第22章
CDC 验证
CDC概念 · 同步器 · 握手/FIFO · 形式化方法
CDC跨时钟
第23章
X-Propagation 验证
X态来源 · 传播路径 · 屏蔽机制 · 形式化检查
X态传播
第24章
Unreachable Code 检测
死代码 · 不可达状态 · 冗余逻辑 · 覆盖率提升
死代码冗余
第25章
Regression 策略
回归测试集 · 形式化回归流程 · 时间管理 · 资源优化
回归自动化
第26章
性能优化
Bounded深度 · 引擎选择 · 并行化 · 内存管理
性能调优
第27章
Debug 与覆盖率分析
反例可视化 · 覆盖点分析 · 未覆盖原因 · 迭代优化
调试分析
第28章
项目实战（一）
项目背景 · 验证计划 · 属性提取 · 环境搭建 · 初步运行
实战项目
第29章
项目实战（二）
深度调试 · 覆盖率分析 · 收敛策略 · 报告总结
实战总结
第30章
形式化验证前沿趋势
机器学习 · 云原生 · AI芯片验证 · 未来方向
前沿趋势