NanDigits中国

GOF Formal介绍

根据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。

Fault模型

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: 影响锥


SPFM和LFM的计算

在详细形式验证处理之前,可以先用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;

相关文档

软件下载


获取评估License



微信公众号

LinkedIn

Nandigits.com 美国官网 | Nandigits.cn 中国官网
© 2022 Nandigits Design Automation. 版权所有。