第三章FSV 功能安全验证
概述
功能安全验证App 面向 ISO 26262 汽车功能安全标准，通过形式方法分析故障（fault）在设计中的传播，验证安全机制（Safety Mechanism）的有效性。
Key Concepts
标准分析技术
FSV 支持以下分析：
- Fault Injection：在设计中注入故障（stuck-at-0/1）
- Fault Propagation Analysis：追踪故障是否传播到安全关键输出
- Fault Detection Analysis：验证安全机制是否能检测到故障
高级形式分析技术
- 故障关系分析（Fault Relations Analysis）
- 多点故障分析
- 故障覆盖度评估
Fault Relations Analysis
分析故障之间的关系：
- Equivalent faults：等效故障（可以合并）
- Dominant faults：支配故障（检测到一个意味着检测到一组）
- Independent faults：独立故障
Setup 和工作流程
FSV 支持两种前端：
- Xcelium Front End：与 Xcelium 仿真器协同
- JasperGold Front End：纯形式验证流程
添加 Faults 和 Strobes
手动添加 Fault
# 添加 stuck-at fault
add_fault -signal u_dut.reg_file[0] -type stuck_at_0
add_fault -signal u_dut.reg_file[1] -type stuck_at_1
# 批量添加 fault
add_fault -hierarchy u_dut.datapath -type stuck_at手动添加 Strobe
Strobe 是观察点，用于检测故障是否被安全机制捕获：
# 添加观察点
add_strobe -signal safety_checker.error_flag -name fault_detected从 Source Browser 添加
在 Source Browser 中右键信号可以直接添加 fault 或 strobe。
Structural Analysis
# 运行结构级故障分析（快速筛查）
analyze_fsv -structural结构分析快速识别哪些故障在结构上无法到达安全输出，无需运行完整证明。
Formal Analysis
# 运行形式故障分析
analyze_fsv -formal
prove_fsv -all形式分析数学证明每个故障是否：
- 被安全机制检测到（Detected）
- 到达安全输出但未被检测（Undetected → 危险）
- 不影响安全输出（Safe）
FSV 功能安全分析界面
功能安全验证方法论
ISO 26262 对形式验证的要求
ISO 26262 汽车功能安全标准要求对硬件故障的影响进行分析。传统方法是故障仿真（在网表中注入故障然后跑仿真），但仿真只能覆盖有限的场景。形式化的 FSV 能穷尽分析所有故障在所有输入条件下的影响，是 ASIL D（最高安全等级）认证的推荐方法。
故障模型选择
| 故障类型 | 模拟的物理故障 | 适用场景 |
|---|---|---|
| SA0/SA1（Stuck-At） | 信号线短路到 VDD/GND | 永久性制造缺陷 |
| SEU（单粒子翻转） | 宇宙射线导致 flop 值翻转 | 软错误（需要时间窗） |
| SET（单粒子瞬态） | 粒子轰击导致信号瞬态脉冲 | 组合逻辑软错误（需要 set_hold_time） |
A/P/D 三维分析
FSV 对每个故障按三个维度分类：
AActivability（可激活性）
故障能被激活吗？即存在输入条件使得故障效应被触发。不可激活→ 该故障永远不可能发生（如恒 0 信号的 SA1 故障），标记 safe。
PPropagatability（可传播性）
激活的故障能传播到输出吗？如果逻辑路径阻塞了传播（如 AND 门另一输入为 0），则故障不可传播，标记 safe。
DDetectability（可检测性）
传播到输出的故障能被安全机制检测到吗？如果有检测器/纠错码/冗余比较等机制捕捉到故障，则 安全（Detected）；如果传到了功能输出且未检测，则 危险（Dangerous）。
安全机制验证思路
验证安全机制有效性的最佳方法是对比实验：
- 在没有安全机制的版本（unsafe）上跑 FSV → 记录 Dangerous 故障数量和类型
- 在加入安全机制的版本（safe）上跑 FSV → 对比 Dangerous 故障减少量
- 减少量就是安全机制的故障覆盖率（Diagnostic Coverage, DC），ISO 26262 要求 DC ≥ 90%（ASIL B）或 ≥ 99%（ASIL D）
来源文档
jaspergold_fsv_userguide.pdfexample_jaspergold_apps/FSV/