第三章FSV 功能安全验证
概述
功能安全验证App 面向 ISO 26262 汽车功能安全标准，通过形式方法分析故障（fault）在设计中的传播，验证安全机制（Safety Mechanism）的有效性。
Key Concepts
标准分析技术（Standard Analysis Techniques）
这一层是结构级故障分析，高度自动化、无需用户干预，用结构上的不可测性（untestability）来预先标注故障集：
- Cone-of-Influence (COI) Analysis：确认 COI 之外的故障节点与 strobe 之间没有物理连接，因此该故障不可测（untestable）。
- Unactivatable Analysis：注入在恒定 0 或恒定 1 节点上的 SA0/SA1 故障，仿真中必然检测不到。若故障节点被永久驱动为所注入的故障值，则该故障 unactivatable。
- Unpropagatable Analysis：已被激活且位于 COI 内、但无法在 functional strobe 上观测到的故障，为 unpropagatable。
高级形式分析技术（Advanced Formal Analysis Techniques）
这一层是形式级分析，支持交互式调试、电路图和传播过程可视化，用于故障分析签核（sign-off）：
- Activation Analysis：检查故障能否从输入被功能性地激活。若不能，判定为 safe。
- Propagation Analysis：检查故障能否传播到 FO。若不能，判定为 safe；若能，则进一步检查它是否总是传播到 FO。
- Detection Analysis：检查故障能否在 CO 上被检测到，以及是否总是被检测到。若是，判定为 safe。
- Correlation Analysis：检查一个已传播的故障是否总能被检测到。若是，判定为 safe。
Fault Relations Analysis
分析故障对（fault pair）之间的关系——因为一个故障的结果可以由另一个故障推断出来。关系分析可用于故障折叠（fault collapsing），减少需要生成的属性数量。关系分为两类：
- Equivalence（等效）：两个位于不同节点的故障，对任意输入激励都产生相同结果。等效关系在仿真前就静态地缩减故障集，把故障分成 prime 故障和 equivalent 故障，只为 prime 故障生成属性。
- Dominance（支配）：当故障 N 在某个输入激励下被检测到（或未被检测到）时，故障 M 也相应地被检测到（或未被检测到）。支配关系通过提取条件化的 Observed/Unobserved 推断关系来缩减故障列表。
Setup 和工作流程
FSV 支持两种前端：
- Xcelium Front End：主要使用流程，依托 Xcelium 前端（xrun）
- JasperGold Apps Front End：次要使用流程，纯形式验证
添加 Faults 和 Strobes
手动添加 Fault
# 初始化 FSV App
check_fsv -init
# 添加 stuck-at 故障（类型写作 SA0 / SA1，可用 + 组合）
check_fsv -fault -add {a b sub.c} -type SA0+SA1
# 批量添加：对 top 下所有 signal 加 SA0+SA1
check_fsv -fault -add [get_design_info -instance top -list signal -silent] -type SA0+SA1
# 对所有 flop 加 SEU；对所有 signal 加 SET
check_fsv -fault -add [get_design_info -instance top -list flop -silent] -type SEU -time_window 0:$
check_fsv -fault -add [get_design_info -instance top -list signal -silent] -type SET -time_window 0:$ -set_hold_time 500ns
# 移除不需要的故障
check_fsv -fault -remove [check_fsv -fault -list -node {.+_failure} -regexp -silent]多重故障注入（Injecting Multiple Faults）
FSV 支持在同一次证明中注入多个故障。你可以指定一组故障，并把"同时注入的故障数"限制为其中的一个子集。check_fsv -fault -add 会返回 fault ID，用这些 ID 就能把先前定义的故障组合起来：
# 先分别定义两个故障（注意它们的时间窗不同）
check_fsv -fault -add { signal_a } -type SA1 -time_window 4cc
check_fsv -fault -add { signal_b } -type SA1 -time_window 6cc
# 用返回的 fault ID 组合成多重故障
check_fsv -fault -add -multiple {0 1}
# 组合时还可以重新指定时间窗（re-timing）
check_fsv -fault -add -multiple {0 1} -time_window 8cc也可以用 -number 指定"从这组故障中最多同时组合几个"：
check_fsv -fault -add { signal_a } -type SA1 -time_window 3cc
check_fsv -fault -add { signal_b } -type SA1 -time_window 2cc
check_fsv -fault -add { signal_c } -type SA0 -time_window 5cc
# 从 ID 2、3、4 这三个故障中，最多同时注入 2 个
check_fsv -fault -add -multiple {2 3 4} -number 2无论原始故障是否发生在同一周期，都可以这样组合。组合后的故障在 Fault Table 的 Type 列中显示为 MULTI——这也是 -type 的合法取值之一（完整取值为 sa0 | sa1 | seu | set | multi）。
手动添加 Strobe
Strobe 是观察点。它分两类：functional（FO）观察功能输出，checker（CO）观察安全机制的输出；默认类型是 functional。
# 在功能输出上加 functional strobe
check_fsv -strobe -add [get_design_info -instance top -list output -include_hier_path -silent] -functional
# 在安全机制（checker）信号上加 checker strobe
check_fsv -strobe -add [get_design_info -list signal -filter "*_failure" -silent] -checker
# 加条件：仅当 valid 为真时才认为故障被观测到
check_fsv -strobe -add {data} -condition {valid}
# 移除某个 strobe
check_fsv -strobe -remove [check_fsv -strobe -list -node top.can_counter_failure -silent]checker strobe 还可用 -checker_mode 指定判定方式：diff（good/bad machine 的 strobe 值不同即算检测到，为默认值）或 assert（bad machine 的 strobe 被置位即算检测到，配合 -assert_value 0|1）。
从 Source Browser 添加
在 Source Browser 中右键信号可以直接添加 fault 或 strobe。
Structural Analysis
# 运行结构级故障分析（快速筛查）
check_fsv -structural
# 可分别控制各项子分析
check_fsv -structural -coi on -constant on -fault_relations on -propagation_analysis on结构分析属于文档所说的"高度自动化的预筛（pre-qualification）流程"——它无需用户干预，用结构上的不可测性分析自动标注故障集。把 FSV 放在故障仿真前后使用，可以缩减故障集、避免无谓的重复仿真。各选项含义：-coi 做 COI 分析并跳过不在 strobe COI 内的故障（可取 on|fo|co|off）；-constant 做 activatability 分析，跳过 unactivatable 故障；-fault_relations 做 dominance 与 equivalence 分析。
Formal Analysis
# 生成 FSV 属性
check_fsv -generate
# 证明 FSV 属性（可加时间上限）
check_fsv -prove -time_limit 1m
# 报告结果
check_fsv -report -class dangerous
check_fsv -report -force -text ~/fsv.rpt形式分析后，每个故障被归入以下 class 之一：safe（安全）、dangerous（危险）、unprocessed（未处理）、unknown（未知）。在 GUI 中分别以绿色、红色、灰色高亮显示。
FSV 功能安全分析界面
功能安全验证方法论
ISO 26262 与功能安全的基本概念
按 ISO 26262 的表述，功能安全指的是：为避免不可接受的人身伤害或财产损失风险，整个系统即使在发生非计划、非预期的事件（故障，fault）时，仍应保持可靠并按预期工作。功能安全的目标是提供冗余和检查器（checker），以便在故障发生时能够恢复。
因此一个功能单元可以表示为一个模块（module）加一个检查器（checker），分别对应功能输出（Functional Output, FO）和检查器输出（Checker Output, CO）——这正是 FSV 中 strobe 分为 -functional 和 -checker 两类的原因。模块内部包含用于纠正故障、阻止故障传播的逻辑。
传统方法是故障仿真（注入故障后跑仿真），但仿真只能覆盖有限的激励场景；文档指出，仿真无法把未观测到的故障判定为 "safe"，只能判为 "not classified"。形式化的 FSV 则可以对故障在所有输入条件下的影响进行穷尽分析。
故障模型选择
| 故障类型 | 故障行为 | 可作用于哪些信号 |
|---|---|---|
| SA0 / SA1 （Stuck-at） | 把信号强制为某个值（0 或 1） | 任意类型的信号（nets 或 registers） |
| SEU （Single Event Upset） | 翻转时序元件输出的值，并保持这个被改变的值，直到它被赋予新值为止 | 仅限时序元件的输出，例如存储器、触发器和锁存器 |
| SET （Single Event Transient） | 翻转信号的值并保持一段时间。该类型必须指定 hold time，例如 SET+500ns | 任意类型的信号（nets 或 registers） |
A/P/D 三维分析
FSV 对每个故障按三个维度分类：
故障能被激活吗？即存在输入条件使得故障效应被触发。不可激活→ 该故障永远不可能发生（如恒 0 信号的 SA1 故障），标记 safe。
激活的故障能传播到输出吗？如果逻辑路径阻塞了传播（如 AND 门另一输入为 0），则故障不可传播，标记 safe。
传播到输出的故障能被安全机制检测到吗？如果有检测器/纠错码/冗余比较等机制捕捉到故障，则 安全（Detected）；如果传到了功能输出且未检测，则 危险（Dangerous）。
两种故障分类方案（Classification Scheme）
安全机制（checker）是否算"把故障管住了"，取决于你选择的分类方案。用 set_fsv_classification_scheme 变量切换：
| 方案 | 判定规则 | 说明 |
|---|---|---|
| iso26262（默认） | 只有 unpropagatable（不可传播）的故障才算 safe | 可传播的故障一律判为 dangerous，无论它是否总能被 checker 检测到 |
| diagnostic | 除 unpropagatable 外，always detected（总被检测到）的故障也算 safe | 把安全机制的检测能力计入安全性判定 |
# 默认为 iso26262；如需把"总被检测到"的故障也算作 safe：
set_fsv_classification_scheme diagnostic
# 查询当前方案
get_fsv_classification_scheme换句话说，同一份设计、同一批故障，在 iso26262 方案下 dangerous 数量会明显多于 diagnostic 方案——因为前者不认可"检测到即安全"。理解这一点，才能正确解读 check_fsv -report -class dangerous 的输出。
来源文档
jaspergold_fsv_userguide.pdfexample_jaspergold_apps/FSV/