01
课程导论：为什么需要协同？
随机激励的局限性，形式化验证的痛点，协同方法论概览。
导论协同
02
SystemVerilog随机化基础
随机变量与约束，`rand`与`randc`，简单约束块，`randomize()`函数。
SV约束
03
SystemVerilog高级约束
条件约束`if-else`，`foreach`约束，`solve...before`，权重分布`dist`。
约束权重
04
SystemVerilog随机化技巧
`post_randomize()`回调，随机化稳定性，`std::randomize()`，数组与队列随机化。
技巧回调
05
覆盖率驱动验证
功能覆盖率概念，`covergroup`与`coverpoint`，交叉覆盖率`cross`，覆盖率选项。
覆盖率covergroup
06
SVA断言基础
`assert`、`assume`、`cover`，序列`sequence`，属性`property`，蕴含操作符`|->`与`|=>`。
SVA断言
07
SVA进阶
带形式参数的序列，`ended`方法，`first_match`，`throughout`与`within`，重复操作符。
序列形式参数
08
SVA时钟与复位
多时钟序列，`$rose`、`$fell`、`$stable`，异步复位断言，`disable iff`。
时钟复位
09
形式化验证工具入门
工具架构（以JasperGold为例），属性编译，`prove`与`cover`命令，反例分析。
工具JasperGold
10
形式化验证环境搭建
`bind`技术，形式化testbench结构，时钟与复位建模，假设管理。
环境bind
11
形式化验证核心概念
有界证明与无界证明，归纳法，k-induction，不变式。
核心归纳
12
形式化验证调试
反例波形查看，`assume`调试，`cutpoint`与`blackbox`，抽象技术。
调试抽象
13
协同验证策略
黑盒与灰盒形式化，激励生成与形式化互补，覆盖率缺口分析。
策略灰盒
14
协同验证流程
从计划到收敛，属性分类，随机测试先行，形式化攻坚。
流程收敛
15
协同验证案例：FIFO
随机写满读空 + 形式化检查空满标志。
FIFO空满
16
协同验证案例：仲裁器
随机激励压测 + 形式化证明公平性。
仲裁公平性
17
协同验证案例：状态机
随机遍历 + 形式化证明死锁/活锁。
FSM死锁
18
协同验证案例：总线协议
随机事务 + 形式化检查协议合规性。
总线协议
19
协同验证案例：安全关键设计
随机故障注入 + 形式化证明安全属性。
安全故障注入
20
协同验证案例：低功耗设计
随机电源状态切换 + 形式化检查隔离与保持。
低功耗电源
21
协同验证案例：Cache一致性
随机请求 + 形式化证明一致性模型。
Cache一致性
22
协同验证案例：浮点运算单元
随机操作数 + 形式化证明IEEE754合规。
浮点IEEE754
23
协同验证案例：DMA控制器
随机描述符 + 形式化证明地址正确性。
DMA地址
24
协同验证案例：加密引擎
随机密钥与数据 + 形式化证明算法正确性。
加密算法
25
协同验证案例：神经网络加速器
随机输入 + 形式化证明数据流正确性。
NN数据流
26
协同验证案例：SoC互联网络
随机路由 + 形式化证明无死锁。
NoC死锁
27
协同验证案例：复位与初始化
随机延迟 + 形式化证明正确退出复位。
复位初始化
28
协同验证案例：错误处理与容错
随机错误注入 + 形式化证明错误响应。
容错错误注入
29
协同验证案例：性能计数器
随机事件 + 形式化证明计数逻辑。
性能计数器
30
课程总结与展望
协同验证成熟度模型，未来趋势（ML辅助形式化，云原生验证）。
总结趋势