📘 形式化验证与断言应用实战 Synopsys VC Formal
🎯 30章 · 从入门到项目
01形式化验证概述
什么是形式化验证与动态仿真区别应用场景与价值
02VC Formal工具入门
工具架构安装与License图形界面/命令行
03SVA基础语法（一）
断言概念立即断言并发断言结构
04SVA基础语法（二）
sequence定义property定义蕴含操作符
05SVA基础语法（三）
时序操作符重复操作符逻辑操作符
06SVA基础语法（四）
$rose/$fell等$stable/$past系统函数
07SVA高级应用
多时钟域断言异步复位断言带参数序列/属性
08断言覆盖率
Coverage语句covergroup结合功能覆盖率分析
09形式化验证流程
Spec提取/建模属性定义证明与反例分析
10VC Formal Tcl脚本基础
Tcl语法入门常用命令启动与运行脚本
11VC Formal Tcl脚本进阶
时钟/复位设置输入约束证明引擎参数
12形式化验证中的约束
assume语句约束优先级约束与断言交互
13反例调试技巧
波形查看反例追踪Debugger定位
14黑盒验证与白盒验证
黑盒方法白盒方法内部信号断言
15有限状态机(FSM)验证
FSM建模状态覆盖断言状态转移断言
16数据通路验证
算术运算验证数据一致性流水线验证
17存储类验证
FIFO验证RAM/ROM验证读写冲突检测
18总线协议验证
握手协议断言AXI/AHB示例时序合规性检查
19安全关键属性验证
死锁检测活锁检测单点故障分析
20形式化与动态仿真结合
动态仿真补充收敛策略混合验证方法
21抽象技术(Abstraction)
数据抽象时间抽象黑盒抽象/大型设计
22VC Formal Proof Engine
引擎类型选择策略性能调优
23形式化验证Reset问题
异步复位同步释放复位序列断言复位对证明影响
24时钟域交叉(CDC)验证
CDC基础形式化CDC方法同步器断言
25低功耗验证
电源域切换断言隔离单元验证电平转换器验证
26形式化验证项目管理
验证计划制定属性评审回归测试策略
27VC Formal Regression模式
批量运行结果汇总报告生成
28常见形式化验证误区
过度约束属性不完备引擎选择/调试效率
29实际项目案例(一)
SPI Slave验证Spec到属性完成
30实际项目案例(二)
多模块互联验证综合运用所学
📢 : 📱 : ✨ 形式化验证 · 断言实战 · 30章全
✧ 风格 · 明亮轻快 ✧