第01章
形式化验证概述
什么是形式化验证 · 为什么需要 · 与仿真测试的区别
概念基础
第02章
验证环境搭建准备
Linux选择 · GCC/G++ · CMake · Python环境
环境工具链
第03章
SystemVerilog断言基础
断言概念 · 立即/并发 · assert/assume/cover · 示例
SVA断言
第04章
SVA序列与属性
sequence · property · 时钟复位 · 蕴含操作符 · 匹配
序列属性
第05章
Formal工具选型
JasperGold · VC Formal · Questa Formal · 选型考量
工具对比
第06章
JasperGold环境搭建
安装 · License · 环境变量 · Tcl交互模式
JasperGold配置
第07章
VC Formal环境搭建
安装 · License · 环境变量 · GUI界面
VC FormalGUI
第08章
Questa Formal环境搭建
安装 · License · 工程管理 · 启动退出
Questa工程
第09章
RTL设计输入
支持风格 · 可综合规范 · 避免语法 · 时钟复位建模
RTL编码
第10章
约束文件编写
时钟/复位约束 · assume · 优先级与冲突解决
约束assume
第11章
覆盖属性编写
cover属性 · 功能覆盖点 · 覆盖率收集 · 空洞分析
cover覆盖率
第12章
证明属性编写
assert · 安全/活性属性 · 不变量 · 有界/无界证明
assert证明
第13章
形式化验证流程
读入设计 · 约束 · 属性 · 证明 · 分析 · 调试反例
流程方法论
第14章
调试反例
波形查看 · 追踪 · 简化 · 与仿真对比 · 修复验证
调试反例
第15章
形式化验证与仿真协同
互补关系 · 协同流程 · 覆盖率互补
协同仿真
第16章
测试插入概念
什么是测试插入 · 目的 · 与DFT的关系
DFT测试
第17章
扫描链插入
扫描链原理 · 插入流程 · 验证 · 故障模型
扫描链DFT
第18章
边界扫描
JTAG标准 · 边界扫描寄存器 · 指令 · 测试
JTAG边界扫描
第19章
内建自测试(BIST)
BIST原理 · 存储器BIST · 逻辑BIST · 控制器
BIST自测试
第20章
测试压缩
数据压缩 · X-tolerant · MISR · 压缩/解压缩电路
压缩MISR
第21章
形式化验证在DFT中的应用
DFT规则检查 · 扫描链形式化 · BIST形式化
DFT形式化
第22章
等价性检查
组合/时序等价性 · 带扫描 · 等价性工具
等价性EC
第23章
属性检查实战
FIFO · 仲裁器 · 状态机 · 总线协议检查
实战属性
第24章
覆盖率驱动验证
覆盖率类型 · 驱动形式化 · 收敛策略 · 报告分析
覆盖率CDV
第25章
抽象技术
抽象概念 · 数据/控制路径 · 抽象精化 · CEGAR
抽象CEGAR
第26章
形式化验证脚本自动化
Tcl · Makefile · Python框架 · 回归集成
脚本自动化
第27章
工业级案例1：CPU核验证
指令集一致性 · 流水线冒险 · Cache一致性
CPU案例
第28章
工业级案例2：总线协议验证
AXI/ACE · 协议状态机 · 数据完整性 · QoS
总线AXI
第29章
工业级案例3：安全模块验证
加密引擎 · 安全启动 · 侧信道防护
安全加密
第30章
形式化验证发展趋势
机器学习 · 云上验证 · 开源工具 · 人才需求
趋势前沿