IP验证中的断言与形式化方法 · 课程目录

断言基础：什么是断言？断言在验证中的角色，断言与形式化验证的关系。

断言角色形式化关系

SVA语法入门：SVA基本结构，序列与属性，关键字(assert, assume, cover)。

序列 assert assume

时序操作符：时钟定义，##延迟，$rose, $fell, $stable边沿检测。

##延迟 $rose $stable

序列组合：连接(##)，交集(and)，或(or)，交叉(intersect)。

## and intersect

属性进阶：蕴含操作符(|=>, |->)，属性嵌套与参数化。

|-> 嵌套参数化

断言覆盖率：cover属性，覆盖率收集意义，分析覆盖率报告。

cover 报告分析

断言调试：失败调试技巧，波形查看断言，定制断言消息。

调试波形消息定制

断言管理：层次化组织，开关控制，断言宏的使用。

层次化开关宏

形式化验证入门：概念，与动态仿真区别，适用场景。

形式化动态仿真

形式化工具介绍：JasperGold, VC Formal, Questa Formal，工作流程。

JasperGold VC Formal

属性检查：SVA属性输入形式化工具，可证明性，反例分析。

可证明性反例

形式化建模：输入约束建模，环境模型构建，抽象与简化。

有界与无界证明：Bounded Proof, Unbounded Proof, 证明深度。

有界无界深度

形式化收敛技术：帮助工具收敛，Assume合理使用，证明引擎选择。

等价性检查：组合等价性，时序等价性，带黑盒等价性。

组合时序黑盒

FPV：形式化属性验证流程，选择属性，FPV与仿真协同。

断言与形式化结合：仿真复用形式化属性，断言库建设。

复用断言库

工业级案例1：总线协议验证(AHB/APB)，断言检查协议，形式化验证总线桥。

工业级案例2：FIFO验证，断言检查满空标志，形式化验证FIFO深度。

工业级案例3：仲裁器验证，断言检查仲裁公平性，形式化验证仲裁算法。

公平性仲裁

工业级案例4：寄存器验证，断言检查读写属性，形式化验证地址译码。

寄存器地址译码

工业级案例5：状态机验证，断言检查状态转换合法性，形式化验证死锁。

状态机死锁

断言重用策略：可重用断言库，断言与VIP(Verification IP)结合。

形式化验证局限性：状态爆炸，复杂数据路径，可行性评估。

状态爆炸数据路径

断言与低功耗验证：低功耗断言，电源域切换形式化验证。

低功耗电源域

断言与安全验证：安全断言编写，信息流形式化验证。

安全信息流

断言与CDC验证：跨时钟域断言，CDC形式化验证方法。

团队协作与流程：断言编写规范，形式化回归流程，版本管理。

未来趋势：AI辅助断言生成，形式化云化，SVA演进。

综合实战项目：从零为IP模块编写断言并形式化验证，总结复盘。