第1章
断言基础
什么是断言？断言在验证中的角色、断言语言概述（SVA/PSL）
核心概念SVA
第2章
SVA语法入门
序列(sequence)、属性(property)、断言指令(assert/assume/cover)
语法序列
第3章
SVA进阶
带参数的序列、局部变量、函数调用、递归属性
参数化递归
第4章
SVA时钟与复位
时钟定义、多时钟域断言、异步复位处理
时钟复位
第5章
SVA匹配操作符
重叠蕴含(|->)、非重叠蕴含(|=>)、ended、throughout、within
蕴含匹配
第6章
SVA重复操作符
连续重复([*n])、非连续重复([=n])、跟随重复([->n])
重复时序
第7章
SVA系统函数
$rose、$fell、$stable、$past、$onehot、$isunknown
系统函数采样
第8章
SVA断言编写实战
FSM状态机验证、FIFO满空标志验证、总线协议验证
实战FSMFIFO
第9章
断言覆盖率
cover指令、覆盖率属性、功能覆盖率与断言覆盖率的区别
覆盖率cover
第10章
断言管理
断言开关、断言层次控制、断言严重性级别、断言错误处理
管理控制
第11章
形式化验证基础
形式化验证概念、与动态仿真的对比、适用场景
形式化概念
第12章
形式化验证流程
属性定义、环境建模、证明引擎选择、结果分析
流程建模
第13章
形式化验证工具
JasperGold、VC Formal、OneSpin 工具链介绍
工具EDA
第14章
形式化环境搭建
时钟建模、复位建模、输入约束、输出检查
环境约束
第15章
形式化验证约束
assume指令、约束编写技巧、过约束与欠约束问题
assume约束
第16章
形式化证明引擎
BDD引擎、SAT引擎、SMT引擎、引擎选择策略
引擎BDDSAT
第17章
形式化收敛技术
抽象技术、归纳法、分解法、引理辅助证明
收敛抽象
第18章
形式化验证调试
反例分析、波形调试、断言细化、环境修正
调试反例
第19章
形式化与仿真协同
动态仿真与形式化验证的互补策略、混合验证方法
协同混合
第20章
总线协议形式化验证
AXI协议验证、AHB协议验证、APB协议验证
AXIAHBAPB
第21章
安全模块形式化验证
安全属性定义、信息流分析、隔离验证
安全隔离
第22章
低功耗形式化验证
电源域切换验证、电压岛隔离验证、低功耗序列验证
低功耗电源域
第23章
数据通路形式化验证
算术单元验证、浮点运算验证、数据一致性验证
数据通路浮点
第24章
控制逻辑形式化验证
仲裁器验证、调度器验证、状态机全覆盖验证
控制仲裁
第25章
存储系统形式化验证
Cache一致性验证、Memory Ordering验证、DMA传输验证
CacheDMA
第26章
复位与时钟域形式化验证
异步时钟域同步验证、复位同步验证、时钟门控验证
CDC复位
第27章
DFT形式化验证
扫描链验证、BIST验证、边界扫描验证
DFT扫描
第28章
SoC集成形式化验证
互联验证、地址映射验证、中断系统验证
SoC互联
第29章
ISO 26262功能安全形式化验证
故障注入验证、安全机制验证、FMEA辅助验证
功能安全26262
第30章
课程总结与项目实战
综合项目实战、常见问题总结、最佳实践分享、未来趋势展望
实战总结