第01章
形式验证概述
什么是形式验证 · 与动态仿真的区别 · 应用场景 · 优缺点
概念基础
第02章
FormalNode工具介绍
工具架构 · 安装与配置 · 基本工作流程 · GUI界面
工具入门
第03章
SVA基础（上）
SVA是什么 · 层次结构 · 序列基本语法 · 属性基本语法
SVA语法
第04章
SVA基础（下）
蕴含操作符 · 重叠与非重叠蕴含 · 时钟定义 · 复位处理
SVA时序
第05章
SVA进阶
带参数序列/属性 · 函数与任务 · 宏定义 · 编译指导语句
SVA高级
第06章
断言覆盖率
断言覆盖率概念 · 覆盖率类型 · 收集方法 · 覆盖率驱动验证
覆盖率指标
第07章
FormalNode基本操作
创建工程 · 导入RTL · 设置顶层 · 编译与语法检查
操作工程
第08章
FormalNode约束编写
时钟/复位/输入/环境约束 · 优先级与冲突解决
约束SDC
第09章
FormalNode断言绑定
直接绑定 · bind文件绑定 · 多断言绑定 · 作用域
绑定断言
第10章
FormalNode属性检查
运行属性检查 · 查看结果 · 分析反例波形 · 调试失败
检查调试
第11章
FormalNode覆盖分析
覆盖属性定义 · 结果查看 · 覆盖点合并 · 报告生成
覆盖分析
第12章
FormalNode调试技巧
GUI调试 · 波形查看 · 断点设置 · Tcl脚本调试
调试技巧
第13章
Tcl脚本基础
Tcl语法 · 变量与列表 · 控制流 · 过程 · 文件操作
Tcl脚本
第14章
FormalNode Tcl自动化
Tcl API · 自动化编译运行 · 批量检查 · 结果分析
自动化Tcl
第15章
FormalNode模式介绍
Prove · Cover · Explain · 模式选择策略
模式策略
第16章
形式化证明引擎
SAT · BMC · k-induction · IC3 · 引擎选择与调优
引擎性能
第17章
抽象与简化技术
抽象概述 · 黑盒/白盒抽象 · 数据/控制路径抽象
抽象简化
第18章
假设保证推理
assume/guarantee指令 · 推理模式 · 应用
推理assume
第19章
形式验证与仿真协同
协同策略 · 激励生成 · 结果反标 · 覆盖率互补
协同仿真
第20章
寄存器验证实战
读写属性 · 复位值 · 保留位 · 寄存器域验证
寄存器实战
第21章
状态机验证实战
状态转换 · 死锁检测 · 可达性 · 等价性检查
FSM实战
第22章
FIFO验证实战
空满标志 · 读写指针 · 深度验证 · 溢出/下溢检测
FIFO实战
第23章
总线协议验证实战
握手协议 · 总线仲裁 · 超时 · 数据完整性
总线协议
第24章
安全属性验证
安全分类 · 信息流分析 · 非干扰 · 机密性与完整性
安全属性
第25章
等价性检查
组合/时序等价性 · 带黑盒等价性 · 应用场景
等价性EC
第26章
形式验证项目管理
验证计划 · 任务分解 · 进度跟踪 · 质量评估
管理流程
第27章
FormalNode性能优化
大规模设计策略 · 并行引擎 · 内存管理 · 运行时间优化
性能优化
第28章
FormalNode常见问题与解决
编译错误 · 约束冲突 · 引擎超时 · 假反例分析
FAQ调试
第29章
FormalNode与其他工具集成
仿真器 · 综合工具 · 覆盖率工具 · 版本管理
集成生态
第30章
综合实战项目
需求分析 · 验证计划 · 断言库 · 约束编写 · 检查调试 · 覆盖率 · 报告
项目综合