Wenhui's Rotten Pen
关于X-Propagation问题

关于X-Propagation问题

本文

主要介绍数字电路设计中X-Propagation问题以及其解决方案。

版本 说明
0.1 初版发布
0.2 添加EDA工具的使用
0.3 添加verilog X-Prop插件VRQ介绍
0.4 添加综合后代码以及仿真结果

参考

什么是 X-Propagation 问题?

什么是 X 状态？

SystemVerilog 标准中定义了四种逻辑状态，即“0”、“1”、“X”、“Z”，“0”代表低电平，“1”代表高电平，“X”代表不定态，“Z”代表高阻态。低电平和高电平很容易理解，而不定态和高阻态只有在模拟仿真时才会出现，真实电路中是不存在“X”和“Z”的。“X”和“Z”都代表不确定是“0”还是“1”的情况，比如未复位前的寄存器，在模拟仿真时是“X”状态，未赋值的悬空信号，在模拟仿真时是“Z”状态。

X 状态的来源有哪些？

数字电路中 X 状态的来源主要有以下几种：

  • 未复位的寄存器和锁存器。
  • 输入信号为 X 状态。
  • 总线竞争。
  • 地址越界。
  • 跨时钟域逻辑（虽然在模拟仿真中不会直观看到X状态，但实际电路中由于跨时钟域是有采样到非理想值的风险，需要关注）。
  • 多驱动（虽然在RTL编码中多驱动认为是一种错误，但实际电路中是有多驱动的技术的）。

总的来说，模拟仿真中 X 的状态更多来自未复位的寄存器和锁存器，尽管可以通过复位信号进行初始化解决这一问题，但是复位信号由于空间和延迟等布线的限制，也并非能够完全做到这一点。尤其现在低功耗设计，电路的睡眠和唤醒机制，对寄存器的初始化设计又带来了复杂性，同时也增加了隐藏 bug 的风险。但是需要注意的是，X 状态在真实电路中是不存在的，要么是“0”，要么是“1”。

什么是 X-Optimism？

RTL 仿真中，对 X 状态是乐观处理的，什么是乐观处理呢？直观来说就是会将一个未知值在电路逻辑中传递为已知值。举例说明：

  • if-else语句
1
2
3
4
5

always@(*)
    if (sel)
        out = a;
    else
        out = b;

结果如下：

sel out
1 a
0 b
x b

在if-else 的选择电路中，当选择信号为 X 时，判断 if 条件不满足，则会执行 else语句，所以 out 值为 b（如果没有 else 语句，则会产生锁存器，保持先前值）。这里补充一下，Z 状态同样会产生相同问题，只不过设计中很少存在 Z 状态，不再讨论。

  • case语句
1
2
3
4
5

always@(*)
    case (sel)
      1: out = a;
      0: out = b;
    endcase

结果如下：

sel out
1 a
0 b
x prev

当选择信号为 X 时，非 0 非 1，不符合 case 语句中任何选项，则保持先前值，这也是将未知状态传递为已知状态的乐观处理。

可见模拟仿真中对 X 状态的乐观处理，与实际电路是有差异的，这样比较容易隐藏功能bug。不过在门级网表仿真中是可以发现这些问题的，门级仿真对 X 状态是悲观处理的，会引入更多无效X状态，而且门级编译和仿真速度很慢，调试也是极其麻烦，将X-Propagation问题放到门级仿真来解决并不是一个好的选择。

什么是 X-Pessimism？

门级网表仿真中，对 X 状态是悲观处理的，什么是悲观处理呢？直观来说就是会将一个已知值在电路逻辑中传递为未知值。举例说明（这里只以assign语句为例，其实所有逻辑综合后都等效为门级电路，换句话说所有逻辑语句在门级电路仿真时都是悲观处理的）：

1

assign out = (a && selector) || (b && ~selector);

结果如下：

selector a b out
X 0 0 X
X 0 1 X
X 1 0 X
X 1 1 X

以上是一个选择器逻辑，当 a 和 b 为相同值时，out结果应该与选择信号无关，也就是当 a和 b 都为“1”时，无论 selector 值为何，其结果值都应该为“1”。而实际门级仿真的悲观处理，在selector为X时，会将结果输出为“X”。

可见门级仿真中对 X 状态的处理是悲观的，这样就会出现不必要的 X 值，与实际电路是有差异的，虽然不会隐藏功能 bug（因为 X 都会暴露出来），但是由此带来的门级仿真和RTL 仿真的差异，必须解决，带来了额外的工作量。

关于clk的X-Prop

以上对选择逻辑的X-Prop问题进行了描述，而对于寄存器来说，clk的X态同样会带来问题，举例如下：

  • 源代码：
1
2

always@(posedge clk)
    q <= d;
  • RTL仿真结果：
clk d q new q
0->X or X->1 0 0 0
0->X or X->1 0 1 0
0->X or X->1 1 0 1
0->X or X->1 1 1 1
  • 真实电路结果：
clk d q new q
0->X or X->1 0 0 0
0->X or X->1 0 1 x
0->X or X->1 1 0 x
0->X or X->1 1 1 1
  • 门级仿真结果：

（注意：猜测结果如下，未进行证实）

clk d q new q
0->X or X->1 0 0 x
0->X or X->1 0 1 x
0->X or X->1 1 0 x
0->X or X->1 1 1 x
  • 总结：

可见对于寄存器关于clk的x态处理，也存在乐观和悲观问题。

结论

通过上面内容，已经知道 X 状态的含义和来源，以及 RTL 仿真对 X 状态的乐观处理和门级仿真对 X 状态的悲观处理，总之由于 X 状态的存在，不同的处理方式，在 RTL 仿真、门级仿真和真实电路之间产生了差异，RTL 仿真的乐观处理，带来了隐藏功能 bug 的风险，门级仿真的悲观处理，当发现 X 状态时首先要确认是真实的 X 状态还是由悲观处理产生的，这带来了额外的工作量，尤其网表调试是极其麻烦的。综上，这就是关于 X-Propagation 问题。

我的测试程序

RTL测试代码

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

module xprop_tb;
reg    clk;
reg    sel;
reg    a0,a1;
reg    b0,b1;
reg    din;

/*AUTOWIRE*/
// Beginning of automatic wires (for undeclared instantiated-module outputs)
wire                    out1;                   // From i_xprop of xprop.v
wire                    out2;                   // From i_xprop of xprop.v
wire                    out3;                   // From i_xprop of xprop.v
wire                    out4;                   // From i_xprop of xprop.v
// End of automatics


initial begin
    //Two options have the same value
    #0  a0=1'b1; a1=1'b1; b0=1'b0; b1=1'b0; #1 sel = 1'bx; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b0; b1=1'b0; #1 sel = 1'bz; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b0; b1=1'b0; #1 sel = 1'b0; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b0; b1=1'b0; #1 sel = 1'b1; #1 $display(out1,out2,out3);

    //Two options have the different value
    #10 a0=1'b1; a1=1'b1; b0=1'b1; b1=1'b0; #1 sel = 1'bx; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b1; b1=1'b0; #1 sel = 1'bz; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b1; b1=1'b0; #1 sel = 1'b0; #1 $display(out1,out2,out3);
    #10 a0=1'b1; a1=1'b1; b0=1'b1; b1=1'b0; #1 sel = 1'b1; #1 $display(out1,out2,out3);

    //test clk
    #10 clk = 1'b0; din = 1'b0; #10 clk = 1'b1; #1 $display(out4);//set out4 pre_value is 0
    #10 clk = 1'b0; din = 1'b1; #10 clk = 1'bx; #1 $display(out4);
    #10 clk = 1'b0; din = 1'b0; #10 clk = 1'b1; #1 $display(out4);//set out4 pre_value is 0
    #10 clk = 1'bx; din = 1'b1; #10 clk = 1'b1; #1 $display(out4);

    #10 $finish;
    end
xprop i_xprop(/*AUTOINST*/
              // Outputs
              .out1                     (out1),
              .out2                     (out2),
              .out3                     (out3),
              .out4                     (out4),
              // Inputs
              .clk                      (clk),
              .sel                      (sel),
              .a0                       (a0),
              .a1                       (a1),
              .b0                       (b0),
              .b1                       (b1),
              .din                      (din));

endmodule // xprop_tb

module xprop (/*AUTOARG*/
// Outputs
out1, out2, out3, out4,
// Inputs
clk, sel, a0, a1, b0, b1, din
);
input clk;
input sel;
input a0;
input a1;
input b0;
input b1;
input din;

output out1;
output out2;
output out3;
output out4;

wire   out1;
reg    out2;
reg    out3;
reg    out4;

assign out1 = sel ? a0 & a1 : b0 | b1;

always@*
    if (sel==1'b1)
        out2 = a0 & a1;
    else
        out2 = b0 | b1;

always@*
    case(sel)
        1'b1: out3=a0 & a1;
        default: out3=b0 | b1;
    endcase

always@(posedge clk)
    out4 <= din;

endmodule // xprop

综合后代码

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

/////////////////////////////////////////////////////////////
// Created by: Synopsys DC Expert(TM) in wire load mode
// Version   : O-2018.06-SP5
// Date      : Mon Feb 24 10:57:14 2020
/////////////////////////////////////////////////////////////


module xprop ( out1, out2, out3, out4, clk, sel, a0, a1, b0, b1, din );
  input clk, sel, a0, a1, b0, b1, din;
  output out1, out2, out3, out4;
  wire   out3, n4, n5;
  assign out2 = out3;
  assign out1 = out3;

  DFFX1_LVT out4_reg ( .D(din), .CLK(clk), .Q(out4), .QN() );
  MUX21X1_LVT U7 ( .A1(n4), .A2(n5), .S0(sel), .Y(out3) );
  AND2X1_LVT U8 ( .A1(a1), .A2(a0), .Y(n5) );
  OR2X1_LVT U9 ( .A1(b0), .A2(b1), .Y(n4) );
endmodule

RTL测试结果

Chronologic VCS simulator copyright 1991-2018
Contains Synopsys proprietary information.
Compiler version O-2018.09-SP2_Full64; Runtime version O-2018.09-SP2_Full64;  Feb 24 17:03 2020
x00
x00
000
111
111
111
111
111
0
1
0
1
$finish called from file "xprop_tb.v", line 39.
$finish at simulation time                  180
           V C S   S i m u l a t i o n   R e p o r t
Time: 180
CPU Time:      0.370 seconds;       Data structure size:   0.0Mb
Mon Feb 24 17:03:52 2020

门级仿真结果

Chronologic VCS simulator copyright 1991-2018
Contains Synopsys proprietary information.
Compiler version O-2018.09-SP2_Full64; Runtime version O-2018.09-SP2_Full64;  Feb 24 17:02 2020
xxx
xxx
000
111
xxx
xxx
111
111
0
x
0
x
$finish called from file "xprop_tb.v", line 39.
$finish at simulation time               180000
           V C S   S i m u l a t i o n   R e p o r t
Time: 180000 ps
CPU Time:      0.360 seconds;       Data structure size:   0.0Mb
Mon Feb 24 17:02:33 2020

总结

  • 使用工具为VCS。
  • 对于综合，无论是三目运算符还是if-else还是case，综合工具都将其转为相同的选择逻辑电路，也就是无论选择RTL何种表达方式，都不影响门级仿真悲观处理的问题，与综合工具也无关，而是仿真工具解析电路的悲观处理导致的。
  • 对于模拟仿真，RTL仿真中if-else和case语句确实存在逻辑乐观处理的问题，而关于三目运算符的结果更符合真实的电路行为； 门级仿真是悲观处理的。

我们的需求是什么？

验证工程师

对于验证工程师，需求是在 RTL 综合之前尽早消除设计中所有 X 传播问题，使其不会隐藏功能 bug，并且不至于在门级仿真中花费大量时间调试 X 传播问题。

这里说明一下为什么在门级仿真中调试 X 传播问题需要消耗大量时间和精力。

  • 综合后的网表不同于 RTL，难以调试定位问题。
  • 由于门级仿真的悲观处理，增加了更多的 X 状态，而且大多是无害的，难以甄别。
  • 门级仿真中发现 X 问题通常体现在输出的功能错误，而抓到错误与实际的 X 产生节点相隔可能多个周期，对调试增加了难度。
  • 门级仿真速度慢.

设计工程师

对于设计工程师，更关心 X 源在设计中的位置，以及 X 在逻辑中的传播，更早的避免、发现和解决 X 传播问题，减少设计代码的迭代，并且最好不需要重新编码以及其他辅助性代码，这样可以依靠工具对代码结构进行静态检查，准确报告有可能存在 X 传播问题的代码信息。当然，对于复杂的低功耗设计，可能会带来更多的 X 传播问题，更有可能隐藏 bug，保证电路功能的正确性是他们最关心的，但对于验证难度也是非常大的。

以往的解决方法

模拟仿真

  • 波形调试工具：波形调试工具会显示 X 状态，在 RTL 仿真和门级仿真不一致时，可以通过波形工具进行调试分析 X 传播问题，当然这是最基础的手动调试方法，除了要排除悲观处理产生的不必要的 X 状态外，在表现为错误的节点和实际产生 X 乐观处理的电路间可能存在多个时钟节拍和复杂的电路层级，这对手动调试都带来了不小的工作，更别说大量的 X 传播问题的存在情况。
  • RTL X 乐观处理的检测：有些仿真工具可以对 X 乐观处理进行检测，当选择条件为 X 状态时，它将驱动 X 状态为 1’b1 和 1’b0，并在两种情况下输出结果不同时报错。这也同

样存在问题，首先是消耗更多的仿真时间，其次是很难保证所有组合状态都已覆盖。

  • 随机初始化值：有些仿真工具支持设置寄存器的初始化值，这样通过初始化值随机化，可以减少大部分的 X 状态，这对于检测悲观处理是个好方法，但对于乐观处理，以及电路正确的初始化，不是一个好方法，首先会掩盖正确初始化的功能验证，其次是如果并未产生导致问题的初始值组合，依然无法发现功能 bug，通过多次随机仿真，不仅消耗了大量的仿真时间，但仍不能保证无隐藏的功能 bug。

代码结构分析

代码检查工具如 Lint，会对代码结构进行分析，以识别潜在的问题，并提醒设计人员可能导致 X 传播问题的危险信息。从代码结构分析来讲，工具会检测逻辑中是否使用了未驱动的信号，诸如这些可能导致 X 传播问题情况。但是代码检查工具并不能确定是否存在真正的问题，这样就需要设计人员去逐个分析。不过好在通过代码检查工具可以定位可能的X源以及与其敏感的电路信号，在发现功能bug时，根据代码检查报告快速定位问题。

形式化验证

  • 等价性检查：很多人都误以为等价性检查会捕获 X 传播问题，而实际并非如此。等价性检查是用于将设计的两个版本（或 RTL 和网表）验证为功能等效。其原理是基于端口信号、黑盒边界以及寄存器初始值的二进制状态空间的遍历。 注：对于此结论并没有完全理解，疑问是形式化验证工具是否对门级网表进行了悲观处理。
  • 模型检查：设计或验证人员使用 SVA 语言编写设计属性，通过形式化验证是状态空间遍历，支持四态的验证工具会验证所有 X 值上无论是“0”还是“1”，都符合设计属性，从而解决 X 乐观和 X 悲观问题。但是需要设计或验证人员编写设计属性，工作量是一方面，还有设计属性描述的完备性以及大规模设计的状态空间爆炸问题难以解决。
  • 符号模型仿真：符号模型仿真可以通过检查输出是否保持一致（无论是否存在 X）来彻底验证设计，并且可以提供反例，显示导致错误的信号状态。但是符号模型仿真也具有局限性，对于大规模的设计会导致内存迅速消耗。同时，设计中可能存在非法输入，可能提供假的反例。 注：对于什么是符号模型仿真本人暂时还不清楚，个人理解为支持X精确的抽象模型。

准确的代码编写

解决 X 传播问题最直接的方法就是准确代码编写，比如双目运算符（？：）是不会被仿真器乐观处理的，可以代替 if-else 和 case，但是它的可读性不强，并且没有避免 X 的悲观处理。那么什么是严格的代码编写呢？举例如下：

  • X-optimistic Coding：当 sel 为 X 时，输出 g 为 2’b01。
1
2
3
4
5

always @(*)
    if (sel==1’b0)
        g = 2’b00;
    else
        g = 2’b01;
  • X-pessimistic Coding：当 sel 为 X 时，输出 g 为 2’bxx。
1
2
3
4
5
6
7

always @(*)
    if (sel==1’b0)
        g = 2’b00;
    else if (sel===1’bx)
        g = 2’bxx;
    else
        g = 2’b01;
  • X-accurate Coding：当 sel 为 X 时，输出 g 为 2’b0x（准确处理的话应该同时包含 Z 的处理，这里没有体现）。
1
2
3
4
5
6
7

always @(*)
    if (sel==1’b0)
        g = 2’b00;
    else if (sel===1’bx)
        g = 2’b0x;
    else
        g = 2’b01;

通过上面的描述感觉问题迎刃而解，仅仅是在编码时追求准确代码编写而已，但是对于赋值语句，很少是常量值，而是复杂的表达式。虽然通过悲观的编码方式可以解决 RTL 仿真的乐观处理问题，但对于门级仿真的悲观处理还是没有解决。

verilog X-Prop插件VRQ

什么是VRQ？

Vrq是一个Verilog工具框架，带有用于处理源代码的各种插件。支持但不完全支持verilog 2005 语法规则。

如何安装？

如何使用？

Vrq支持的插件功能很多，这里仅以X-Prop为例，使用命令为： “vrq -tool xprop source.v -o target.v” 。这里也就是将source.v源代码进行X-Prop处理，处理完毕后的代码输出至target.v。效果如下：
vrq xprop处理前：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

module top_module ();
    reg clk;
    wire out1;
    reg out2;
    reg out3;
    reg sel;

    reg a0,a1;
    reg b0,b1;

    reg out4;
    reg din;

    assign out1 = sel ? a0 & a1 : b0 | b1;

    always@*
        if (sel==1'b1)
                out2 = a0 & a1;
        else
                out2 = b0 | b1;

    always@*
        case(sel)
            1'b1: out3=a0 & a1;
            default: out3=b0 | b1;
        endcase

    always@(posedge clk)
        out4 <= din;
endmodule

vrq xprop处理后：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

//****************************************
// Warning! This file is machine generated
//****************************************


module top_module();
    reg clk;
    wire out1;
    reg out2;
    reg out3;
    reg sel;
    reg a0;
    reg a1;
    reg b0;
    reg b1;
    reg out4;
    reg din;
    assign   out1=sel ? a0&a1 :
        ~sel ? b0|b1 : 1'hx;
    always @* if(sel==1'b1) begin
        out2 = a0&a1;
    end else if(~(sel==1'b1)) begin
        out2 = b0|b1;
    end else begin
        out2 = 1'hx;
    end
    always @* case(sel)
        1'b1: begin
            out3 = a0&a1;
        end
        default: begin
            case(sel)
                1'b0,
                1'b1: begin
                    out3 = b0|b1;
                end
                default: begin
                    out3 = 1'hx;
                end
            endcase
        end
    endcase
    always @(posedge clk) out4 <= din;

endmodule


//****************************************
// Warning! This file is machine generated
//****************************************

可见vrq xprop插件自动完成了将常规逻辑语句准确的xprop语句，简化了工程师的编码工作。关于vrq的xprop的详细功能，可通过“vrq –help”或“man vrq” 查看。

其他功能

vrq支持的verilog源代码处理插件很多，可通过“vrq –help”或“man vrq” 查看。由于其他功能没有亲自实践，这里不再描述，待后续补充。

最新EDA工具的支持

VCS 的 X-Propagation 功能

VCS X-Prop 的介绍

X-Propagation 是 VCS 开发的用于 RTL 阶段发现 X 态问题的新增特性。该特性主要有两种使用模式：T-merge 和 X-merge。T-merge 采用的算法是：当所有可能值不同时，结果为 X；X-merge采用的算法是：无条件的结果为 X（门级仿真的悲观处理）。下面对 T-merge 和 X-merge 举例说明：

1
2
3
4
5

always@(*)
    if (select)
        out <= a;
    else
        out <= b;

看一下 T-merge 和 X-merge 的对比：

select a b T-Merge X-Merge
X 0 0 0 X
X 0 1 X X
X 1 0 X X
X 1 1 1 X

使用方法

只需在 VCS 仿真中添加-xprop 或者-xprop=xmerge 选项，默认是 T-merge 模式。也可以通过配置文件指定哪些模块使用 X-propagation 功能，以及指定使用哪种模式，其使用方法为： vcs -xprop=xp_config_file… 配置文件内容格式如下：

tree {bridge} {xpropOff};
instance{top.bridge.cpu}{xpropOn};
module {sram,cache}{xpropOff};
merge = tmerge;

另外boundscheck 的使用可以抓到数组下标不合法问题，不合法的下标分两类，下标越界和下标为 X。使用方法是在编译时添加-boundscheck 选项，运行仿真时会检查下标问题，输出报告。

结论

  • X-Propagation 简单易用。
  • 使用 T-merge 可以让各种语法结构中的 X 态问题有效传播，其效果可以代替门级仿真，但仿真速率要优于门级仿真。
  • 建议使用方法为：先使用 T-merge 模式，当回归 pass 后再使用 X-merge 模式，如果 pass 则 OK，如果 fail 需要检查是否无效 fail。
  • 使用 X-Propagation 对仿真性能影响可接受，T-merge 模式影响更小（注：与Cadence相反，待考证）。
  • 对于低功耗设计由于其电源控制的复杂性，更有必要使用 X-Propagation。

INCISIVE 的 X-Propagation 功能

INCISIVE X-Prop 的介绍

INCISIVE13.1及更高版本，开始支持X-prop的功能，该功能通过命令行上的’-xprop <F / C>'选项启用。

X-Prop工具目的是在RTL仿真中尽早的发现并解决X问题，其特点如下：

  • 两种X-Prop模式
    • FOX模式 (“Forward only X”)
    • CAT模式 (“Compute as Ternary”)
  • 这两种模式可以区别LRM（Language Reference Manual）的行为
  • 不需要更改现有的设计
  • 减少门级调试

测试代码：

1
2

if( sel) out = a;
else out = b;

两种模式结果对比：

sel a b out(verilog LRM) out(FOX model) out(CAT model)
x 0 0 0 x 0
x 0 1 1 x x
x 1 0 0 x x
x 1 1 1 x 1

使用方法

只需要在 INCISIVE 仿真中添加-xprop选项，该选项包含在xrun中，命令为“xrun –xprop F|C”，这里F代表FOX模式，C代表CAT模式。而且可以提供配置文件以在选定的层次结构/实例上启用X-Prop，这也是最推荐的方式，命令为“xrun –xfile <file_name>”，Xfile格式如下：

//在CAT模式下，在testbench以及其子模块中启用xprop
SCOPE testbench… C
//在FOX模式下，在testbench.dut以及其子模块中启用xprop
SCOPE testbench.dut… F

为了降低调试的难度，在较大设计中，可以为少量模块添加X-Prop，这可以在Xfile中实现：

SCOPE TB.DUT_TOP.AHB_MOD1…C
SCOPE TB.DUT_TOP.CPU… C
SCOPE TB.DUT_TOP.APB_MOD2… C
SCOPE TB.DUT_TOP.AHB3… C

运行仿真时可以使用tcl命令控制开启和关闭X-Prop：

xrun> xprop -off // Disable X-Propagation
xrun> run 10ns
xrun> xprop -on // Enable X-Propagation

结论

  • FOX模式比CAT模式仿真速度更快，因为FOX模式对x强制传播，无额外判断。
  • 关于发现X bug，使用CAT模式更依赖于输入激励的质量，有可能由于判断逻辑选择值相同而继续被掩盖。
  • FOX模式更近似于门级仿真的行为。
  • 建议从单元级模块运行X-Prop，待单元级模块清除X-Prop问题，然后在系统级运行X-Prop。
  • 建议先使用CAT模式，将真实的X-Prop问题处理完毕后，再使用FOX模式。

JasperGold 的 X-Propagation 功能

JasperGold X-Prop APP 的功能

  • 检查时钟和复位，以确保无Xs。
  • 检查赋值逻辑，以确保无Xs
  • 检查控制逻辑，以查看Xs可以传播到哪些区域。
  • 检查输出信号，以查看Xs是否可以传播到设计之外。
  • 检查黑盒输入，以查看Xs是否可以传播到黑盒上层模块。
  • 可使用 assume-guarantee 的方法，使对X-Prop问题的证明尽可能收敛。

启动命令

jg -xprop

待补充

以目前的了解，JasperGold X-Prop是需要工程师选定X源，然后工具为其进行0 1状态遍历，检查输出是否一致，若不一致则证明X传播至设计外部，可能存在设计bug，需要工程师去调试分析。形式化验证工具的好处就是工具自动采用状态空间全遍历的引擎，这对一个设计的完整验证似乎更有保证，防止模拟仿真中测试激励质量的问题而隐藏bug，但是形式化验证更适合单元级模块，较大模块会带来状态空间爆炸的问题，无法证明完全。这里另外说明一下可能的X源，其中最主要的就是输入信号和未复位状态的寄存器，如果选择输入信号作为可能的X源，我想不应该必然会影响设计输出吗？

至于JasperGold X-Prop对X源的设定和分析，工具如何使用和调试，以及其工作原理，本人并未实际使用过，待通过工程实践后再补充。

总结

X-Prop问题一直存在，由于现在设计规模越来越大，功耗控制技术越来越复杂，X-Prop问题显得更为重要，从以往的解决办法中，认为准确的代码编写最为有效，而且有工程师为其开发的脚本工具，但是个人认为不能很好的解决悲观问题，不过好在模拟工具都对X-Prop做了很好的支持，我们只要用好工具就能做到事半功倍。

另外，如有兴趣欢迎详细交流和分享。

文章原创，可能存在部分错误，欢迎指正，联系邮箱 cao_arvin@163.com。

文章目录