01
形式化验证概述
什么是形式化验证 · 与动态仿真的区别 · 应用场景
基础概念
02
覆盖死角的概念
覆盖死角定义 · 产生原因 · 对验证质量的影响
核心死角
03
断言基础
SVA语法 · 立即断言与并发断言 · 在覆盖死角中的作用
断言SVA
04
覆盖组与覆盖点
covergroup语法 · coverpoint与bin · 交叉覆盖
覆盖SV
05
形式化属性检查
property定义 · sequence用法 · assert/assume/cover
属性检查
06
有界模型检查(BMC)
BMC原理 · 深度设置 · 覆盖死角检测
BMC有界
07
无界模型检查
无界原理 · 归纳法证明 · 与BMC对比
无界归纳
08
形式化引擎介绍
SAT求解器 · BDD引擎 · SMT求解器 · 选择策略
引擎SAT
09
假设保证推理
assume指令 · 环境约束建模 · 假设与覆盖
假设推理
10
覆盖导向的形式化验证
覆盖驱动流程 · 目标设定 · 工具利用覆盖信息
覆盖导向流程
11
死代码与不可达状态
死代码检测 · 不可达状态分析 · 消除冗余
死代码不可达
12
状态空间爆炸问题
爆炸原因 · 抽象技术 · 对称性简化 · 应对策略
爆炸抽象
13
抽象技术
谓词抽象 · 数据抽象 · 控制抽象 · CEGAR
抽象CEGAR
14
等价性检查
组合与时序等价性 · RTL与门级网表检查
等价性RTL
15
模型检验
CTL与LTL · 模型检验算法 · Kripke结构
模型检验时序
16
符号模型检验
符号表示 · BDD应用 · 优缺点
符号BDD
17
有界模型检验与SAT
SAT编码 · 增量SAT · BMC工业应用
SATBMC
18
形式化验证工具
JasperGold · VC Formal · OneSpin · 开源工具
工具工业
19
断言覆盖率分析
断言覆盖率定义 · 收集 · 与功能覆盖率结合
断言覆盖率
20
覆盖死角的形式化检测方法
自动寻找未覆盖 · 反例分析 · 覆盖空洞定位
死角检测反例
21
属性综合与挖掘
自动属性生成 · 数据挖掘 · 从波形提取属性
挖掘综合
22
并发与互斥验证
死锁/活锁检测 · 互斥协议 · Petri网
并发互斥
23
协议验证
总线协议 · 握手协议 · AMBA AXI/AHB形式化
协议AMBA
24
安全属性验证
信息流分析 · 非干涉属性 · 安全漏洞检测
安全信息流
25
形式化验证与仿真协同
混合验证 · 引擎交互 · 覆盖率互补
协同混合
26
回归验证中的形式化
回归重用 · 增量验证 · 变更影响分析
回归增量
27
形式化验证的调试技巧
反例可视化 · 波形调试 · 属性/假设调试
调试反例
28
覆盖率驱动的形式化收敛
设定覆盖目标 · 迭代精化 · 收敛标准与退出
收敛迭代
29
工业案例
处理器验证 · 存储控制器 · DMA控制器
案例工业
30
形式化验证的未来趋势
机器学习辅助 · 云上形式化 · 形式化与AI结合
未来AI