硬件与芯片设计形式化验证解决方案
未定义行为与微架构侧信道的数学证明
基于等价性检查与信息流验证的芯片验证方法
为什么传统方法在芯片验证领域已经不够？
RTL 级非确定性行为
竞争条件导致仿真通过但硅片失败，传统验证无法覆盖所有时序组合
缓存推测执行侧信道
Spectre/Meltdown 类漏洞通过微架构状态泄露敏感信息
协议死锁活锁
AXI/CHI 总线协议请求 - 响应组合状态空间爆炸，测试遗漏异常序列
形式化验证如何重构信任？
01
等价性检查 (EC)
证明 RTL 实现与体系结构规范（指令集模型）完全一致，无功能偏差
02
符号执行验证
使用符号执行探索所有可能的数据路径，发现隐蔽的逻辑漏洞
03
信息流验证
检测缓存/分支预测器是否存在可被利用的信息流路径，对抗侧信道攻击
04
协议模型检验
验证总线协议所有请求 - 响应组合无活锁/无丢失/无死锁
交付物及通过的行业标准
核心交付物
- RTL 到黄金参考模型的组合等价性证明
- 非干扰（non-interference）证书（对抗侧信道）
- 协议形式化验证报告
- 侧信道脆弱性分析报告
支持的标准认证
ISO 26262
ASIL-D
DO-254
Level A
Common Criteria
EAL6+
客户案例
客户行业
某 RISC-V 处理器设计公司
验证前
传统 UVM 验证 18 个月，流片后发现 2 处 MMU 权限逃逸漏洞
验证后
形式化验证发现 4 处特权级检查缺失，修复后一次流片成功
流片风险降低 85%
技术规格
输入支持
- •Verilog/SystemVerilog RTL
- •VHDL
- •Chisel
- •指令集规范文档
输出格式
- •等价性证明报告
- •信息流验证证书
- •协议验证日志
- •自然语言分析报告
验证工具链
- •Cadence JasperGold
- •Synopsys VC Formal
- •自定义符号执行引擎