形式化验证入门

📚 30章 · 电路验证 🎯 风
01 形式化验证概述
什么是形式化验证 为什么需要形式化验证 与仿真验证对比
02 数学基础
命题逻辑 谓词逻辑 布尔代数基础
03 模型检测入门
基本概念 状态空间 状态转移系统
04 时序逻辑基础
线性时序逻辑(LTL) 计算树逻辑(CTL) CTL*
05 模型检测算法
显式状态模型检测 符号模型检测(BDD) 有界模型检测(SAT/SMT)
06 属性规约语言
SystemVerilog Assertion (SVA) 基础 断言类型与层次
07 SVA序列与属性
序列(sequence)定义 属性(property)定义 蕴含操作符
08 SVA进阶
多时钟域断言 函数与任务 宏定义
09 形式化验证工具
JasperGold / VC Formal / OneSpin 工具选型考量
10 形式化验证流程
验证计划制定 属性提取 环境搭建 调试与收敛
11 属性提取方法论
从规格文档提取 从设计意图提取 从仿真波形提取
12 形式化验证环境搭建
顶层模块封装 时钟与复位建模 输入约束建模
13 输入约束与假设
assume指令 公平性约束 环境建模最佳实践
14 覆盖分析与证明完备性
cover指令 证明深度 覆盖度量指标
15 调试技术
反例分析 波形调试 属性细化
16 抽象技术
数据路径抽象 控制路径抽象 黑盒与白盒抽象
17 等价性检查
组合等价性检查 时序等价性检查 带黑盒的等价性检查
18 形式化验证在SoC中的应用
总线协议验证 中断控制器验证 电源管理验证
19 形式化验证在安全中的应用
信息流分析 安全属性验证 侧信道攻击检测
20 形式化验证在FPGA中的应用
综合后网表验证 时序收敛验证 配置逻辑验证
21 形式化验证与仿真协同
动态仿真与形式化互补 混合验证策略
22 形式化验证与覆盖率驱动验证
功能覆盖率与形式化覆盖 断言覆盖率
23 形式化验证中的性能优化
BDD变量排序 SAT求解器调优 并行化策略
24 形式化验证的局限性
状态爆炸问题 可扩展性挑战 适用场景判断
25 工业级案例1：AMBA AHB总线协议验证
AHB总线协议验证实战
26 工业级案例2：FIFO控制器形式化验证
FIFO控制器验证实战
27 工业级案例3：仲裁器公平性验证
仲裁器公平性验证实战
28 形式化验证团队建设
技能要求 团队角色 流程规范
29 形式化验证的未来趋势
机器学习辅助验证 云上形式化验证 开源工具发展
30 课程总结与进阶路径
关键知识点回顾 推荐书籍与论文 社区与资源
📘 电路验证中的形式化验证入门 专注资料整理 ✨ 30章完整目录