name: formal-verification description: FPGA设计的正式属性验证与模型检验技能 allowed-tools:
- Read
- Write
- Edit
- Glob
- Grep
- Bash
正式验证技能
概述
用于正式属性验证和模型检验的专家级技能，无需仿真即可对FPGA设计属性进行穷尽性验证。
能力
- 编写用于正式验证的属性
- 配置正式工具约束
- 分析正式反例
- 应用有界模型检验
- 配置覆盖和假设指令
- 调试正式验证失败
- 将正式验证与仿真流程集成
- 支持JasperGold和VC Formal流程
目标流程
- sva-development.js
- cdc-design.js
- constrained-random-verification.js
使用指南
属性类型
- assert property: 必须始终成立
- assume property: 环境约束
- cover property: 可达性目标
- restrict property: 强约束
正式验证方法
- 有界模型检验: 检查最多N个周期的属性
- 无界证明: 在可能的情况下进行完整验证
- 归纳法: 用于活性属性的K-归纳
- 抽象化: 为可扩展性降低复杂性
编写有效属性
// 安全性属性
assert property (@(posedge clk) disable iff (rst)
req |-> ##[1:5] gnt);
// 活性属性（有界）
assert property (@(posedge clk) disable iff (rst)
req |-> s_eventually gnt);
// 正式验证的假设
assume property (@(posedge clk)
$onehot0(req_vec));
约束开发
- 建模输入协议约束
- 约束不现实的场景
- 避免过度约束
- 对复杂约束使用辅助逻辑
- 记录约束原理
反例分析
- 加载反例追踪
- 识别根本原因
- 区分错误与缺失约束
- 根据反例创建回归测试
- 更新约束或修复RTL
工具集成
- 配置引擎选择
- 适当设置证明边界
- 使用证明加速技术
- 与回归流程集成
- 归档证明结果
依赖项
- 正式工具认知（JasperGold, VC Formal）
- SVA专业知识
- 模型检验理论知识