NanDigits中国
根据ISO26262标准，汽车芯片都有功能安全的需求。具体来说，single point fault metric (SPFM)和latent fault metric (LFM) 应该要满足ASIL等级的最低要求。
| ASIL | SPFM | LFM |
|---|---|---|
| B | ≥90% | ≥60% |
| C | ≥97% | ≥80% |
| D | ≥99% | ≥90% |
用传统的动态仿真来计算显得效率比较低。GOF Formal提供了一种形式验证的方法，可以高效的计算设计中的SPFM和LFM。
GOF Formal对设计的每一个输入端口和逻辑门的每一个pin进行注入故障。每个输入端口都可以注入stuck-at 0和stuck-at 1故障。每个组合逻辑的pin也被注入stuck-at 0和stuck-at 1故障。 对于触发器，stuck-at 0和stuck-at 1被注入到时钟和数据pin，在任意时间内，触发器的状态被注入Single Event Upset(SEU)类型的故障。
图 1: 逻辑门的故障模型
基于影响锥进行结构化的分析和详细得分计算。影响锥的抽取定义了两种类型的选通点：
观察点就是受故障注入影响到功能安全的输出或者寄存器。检测点是用来检查是否受到故障注入影响的输出或寄存器。
从观察点和检测点开始往回追逻辑，找到与输入或者遇到黑盒子的之间所有的通路。这样，观察点和检测点的影响锥（COI）就创建了。逻辑锥里的每个cell将会被根据故障模型注入故障。
图 2: 影响锥
在详细形式验证处理之前，可以先用COI结构化分析运行一次快速的故障覆盖率。
在图2中，两个COI的外部的所有故障都是安全故障。
A区域故障可以观察到的但检测不到，所以，如果B区域为0，这些故障可被分类到residual故障或者单点故障。
因为B区域是既可以观察到又可以被检测到，所以B区域就分类为多点故障。
C区域被分类到可检测的多点故障，但是不可观察到。在B和C区域运行形式验证，来检查是否这些故障不可传播到检测点。如果可以，那么就被分类到潜在（latent）故障。
The Single Point Fault Metric (SPFM) 可以根据下面的公式来计算：
SPFM = 1 - Σ(λSPF+λRF)/Σ(λ)
The Latent Fault Metric (LFM) 可以根据下面的公司来计算：
LFM = 1 - Σ(λMPF_UD)/Σ(λMPF - λSPF - λRF)
在快速分析中, Σ(λSPF+λRF) 是A区域的故障。Σ(λMPF_UD) 是不可观察并不可检测到故障。 在快速分析中，LFM是100%，既然在COI结构里不存在同时为不可观察和不可检测的故障。
运行形式验证来调整得到最终结果。对每一个注入的故障，GOF Formal要么证明传播故障到观察点或检测点的路径存在，要么证明路径不存在。这样的一条路径可以在有限的时钟内，通过toggle输入端口，把故障传播到观察点或者检测点。
GOF Formal不需要外部激励，也不需要testbench，而是由GOF Formal自己产生激励。对每个注入的故障，对比两个设计来判断是否指定的输出端口是等价的。一个设计是故障注入的设计，另一个是原始设计。指定的输出端口可以由用户指定为观察点或者检测点。要注入的故障很多，有几千或者数百万个。GOF Formal可以充分利用使用计算机集群的算力来计算。而几千个job提交到集群上并行计算只需要一个license。
SPFM和LFM的计算例子：
set_log_file("spfm_lfm.log"); # Set log file name read_library("art.5nm.lib"); # Read in liberty file read_design('-imp', 'ecc_process.v'); # Read in the design block set_top("ecc_top"); # Set the top module name set_pin_constant("test_mode", 0); # Set pin constraint set_observe_points("data_out*"); # data_out[31:0] affects functional safety set_observe_points("synd_out"); # synd_out affects functional safety set_detect_points("sb_err_o"); # Safety mechanism detecting output set_detect_points("db_err_o"); # Safety mechanism detecting output verify_faults("-full"); # Calculate and print SPFM and LFM, Use verify_faults("-coi") for fast SPFM/LFM calculation gexit;
verify_faults API可以运行单个故障，来检查是否故障可以传播到观察点。如果故障可观察，就会dump一个VCD波形来显示怎样按时钟周期toggle输入端口来传播故障。所有的内部信息也会抓出来一起放在VCD文件里。
下面的脚本用来检查是否SEU故障能够传播。如果可以，就dump vcd波形：
set_log_file("spfm_lfm.log"); # Set log file name read_library("art.5nm.lib"); # Read in liberty file read_design('-imp', 'ecc_process.v'); # Read in the design block set_top("ecc_top"); # Set the top module name set_pin_constant("test_mode", 0); # Set pin constraint set_observe_points("data_out*"); # data_out[31:0] affects functional safety set_observe_points("synd_out"); # synd_out affects functional safety # To check if the fault can be propagated to the detect points, set_observe_points on the detect points verify_faults("u_ecc_ops/bit_reg:SEU", "-vcd", "debug_seu.vcd"); # Check if the Single Event Upset on the flop can propagate gexit;
