Question

使用一个SystemVerilog静态变量意味着仅存在它的一份拷贝。如果需要在流水线设计中检查数据值，那么对于每一个进入流水线的数据量值，我们可以使用一个单独的变量来存储预期的流水线输出，以便在真正退出管线的时候比较结果。这个存储空间可以通过使用一个变量数组来构建，并且为了最小化通过流水线的传播这个数组可以安排在一个移位寄存器中。然而，在一些更为复杂的情况下，例如管线的潜伏期是可变的并且是乱序的，那么这种结构可能就变得非常复杂并且容易出错。因此，我们需要一些局部变量，这些变量在一个特定的、能够跨越任意时间间隔的事务检查中使用，并且能够与其它事务检查重叠。所以，这样的一个变量必须能够在需要的时候在一个序列实例中动态地产生并能在序列结束的时候移除。

一个变量的动态产生极其赋值是通过在一个序列或特性声明中使用局部变量声明并在序列中赋值来实现的。

sequence_expr ::=         // 引用自附录A.2.10
    ...
  | (expression_or_dist{, sequence_match_item}) [boolean_abbrev]
  | (sequence_expr{, sequence_match_item}) [sequence_abbrev]
    ...

语法 17-12 — 变量赋值语法（摘录自附录A）

变量的类型被显式地说明。通过将子序列、采样赋值放置在圆括号中并以逗号分割，变量可以在任意符合语法的子序列的结束点上被赋值。例如，如果在下面的序列中：

a ##1 b[->1] ##1 c[*2]

我们希望在b[->1]的匹配上作这样的赋值：x = e，那么序列可以按如下方式重写：

a ##1 (b[->1], x = e) ##1 c[*2]

以后，局部变量可以在序列中按如下的方式被重新赋值：

a ##1 (b[->1], x = e) ##1 (c[*2], x = x + 1)

对于每一次尝试，都会为序列产生变量的一个新的拷贝。变量值可以向任何其它SystemVerilog变量一样被测试。

不允许层次化地引用局部变量。

考虑一个局部变量使用的例子，假设一个流水线具有固定的5个时钟周期的潜伏期。当valid_in为“真”的时候，pipe_in携带数据进入管线，并且流水线计算的值在5个时钟周期之后出现在信号pipe_out1上。管线传输的数据通过一个函数来预测，这个函数对数据进行递增。下面的特性验证了这个行为：

property e;
    int x;
    (valid_in,(x = pipe_in)) |-> ##5 (pipe_out1 == (x+1));
endproperty

特性e按如下方式计算：

1. 当valid_in为“真”的时候，x被赋值为pipe_in的值。如果5个周期之后，pipe_out1等于x+1，那么特性e为“真”。否则特性e为“假”。
2. 当valid_in为“假”的时候，特性e计算成“真”。

变量可以在序列或特性中使用。

sequence data_check;
    int x;
    a ##1 !a, x = data_in ##1 !b[*0:$] ##1 b && (data_out == x);
endsequence

property data_check_p
    int x;
    a ##1 !a, x = data_in |=> !b[*0:$] ##1 b && (data_out == x);
endproperty

局部变量可以在重复的序列上写入并实现值的累加。

sequence rep_v;
    int x;
    `true,x = 0 ##0
    (!a [*0:$] ##1 a, x = x+data)[*4] ##1 b ##1 c && (data_out == x);
endsequence

局部变量在这个序列被实例化的序列中是不可见的。下面的例子演示了在序列seq1中对子序列sub_seq1中局部变量v1的无效访问。

sequence sub_seq1;
    int v1;
    a ##1 !a, v1 = data_in ##1 !b[*0:$] ##1 b && (data_out == v1);
endsequence

sequence seq1;
    c ##1 sub_seq1 ##1 (do1 == v1); // 错误的，因为v1是不可见的。
endsequence

为了访问一个子序列的局部变量，必须声明一个局部变量并通过一个自变量传递到被实例化的子序列。下面的例子演示了这样的用法。

sequence sub_seq2(lv);
    a ##1 !a, v1 = data_in ##1 !b[*0:$] ##1 b && (data_out == lv);
endsequence

sequence seq2;
    int v1;
    c ##1 sub_seq2(v1) ##1 (do1 == v1); // 现在v1被绑定到lv
endsequence

局部变量可以被传递到一个应用了ended的命名序列的实例，并且以相似的方式访问。例如：

sequence seq2a;
    int v1;
    c ##1 sub_seq2(v1).ended ##1 (do1 == v1); // 现在v1被绑定到lv
endsequence

当将局部变量可以被传递到一个应用了ended的命名序列的实例的时候存在一些限制：

1. 局部变量只能以完整的实型参数传递，而不能作为实型参数的正确子表达式传递。
2. 在命名序列的声明中，局部变量被绑定的形式参数不能在它被赋值之前引用。

sub_seq2符合第二条限制，因为v1 = data_in的赋值发生在data_out == lv中对lv的引用之前。

如果一个局部变量在被传递到一个应用了ended的命名序列的实例之前进行了赋值，那么上述的限制能够防止所赋的值在命名序列内部可见。这些限制是重要的，因为ended的使用意味着局部变量在命名序列外部被赋值的时间点与实例匹配的起始点没有能够得到保证的关系。

如果下面两个条件被满足，一个作为实形参数被传递到一个应用了ended的命名序列的实例的局部变量将会从ended的应用中流出到该实例：

1. 局部变量流出命名序列实例的结尾，如序列的局部变量流规则所定义的那样。（参见下面的描述以及附录H。）
2. 作用到该实例的ended的应用是一个最大的布尔表达式。换句话说，ended的应用上不能有非或任何其它表达式操作符。

上述的两个条件均被sub_seq2和seq2a所满足。因此，seq2a中比较表达式do1 == v1中v1的值为sub_seq2中通过赋值语句v1 = data_in赋给lv的值。 然而，对于下面的例子：

sequence seq2b;
    int v1;
    c ##1 !sub_seq2(v1).ended ##1 (do1 == v1); // v1 unassigned
endsequence

上面的例子违背了第二个条件，因为“非”操作被应用到了sub_seq2(v1).ended。因此，v1不会从ended的应用中流出到这个实例，并在表达式do1 == v1中对v1的引用是一个未赋值的变量。

在单个周期中，一个应用了ended的序列实例可能具有多个匹配，并且这些匹配对本地变量可能具有不同的计算结果。在语义上，多个匹配按匹配一个or操作的两个析取项相同的方式对待（参见下面的描述）。换句话说，计算应用了ended的实例的线程将会产生分支以便单独地考虑这些局部变量。

注意：当一个局部变量是一个序列声明的形式参数的时候，按如下所示的方式声明变量是非法的。

sequence sub_seq3(lv);
    int lv; // 因为lv是一个形式参数，所以该条声明是非法的。
    a ##1 !a, v1 = data_in ##1 !b[*0:$] ##1 b && (data_out == lv);
endsequence

当在调用分支操作符or、and以及intersect的序列中使用局部变量的时候，必须作出一些特别的考虑。从这些操作符的一个构建而来的复合序列的计算可以认为是产生两个分支线程来并行地计算操作书序列。在开始计算复合序列之前一个局部变量可能已经被赋了值。这样的一个局部变量被称为流入到每一个操作数序列。局部变量可以在一个或两个操作数序列中被赋值或解赋值。通常，我们不能保证两个线程的计算会产生一致的结果值，乃至对局部变量是否已经被赋了值具有一致的认识。因此，在复合序列的计算过程中或之前赋给局部变量的值并不总是被允许在复合序列的计算之后可见。

在某些情况下，在局部变量值上的不一致是无关紧要的，然而在有些情况下却是重要的。附录H给出了一些精确的条件来定义一些静态（也就是编译时可计算的）条件，在这些条件下能够保证局部变量的值在复合序列被计算后具有一致的视图。如果满足了这些条件，那么局部变量被称为流出了复合序列。局部变量流的一个直观描述如下：

1. 在并行线程上赋值的变量不能在同属线程中访问。例如：

sequence s4;
    int x;
    (a ##1 b, (x = data) ##1 c) or (d ##1 (e==x)); // 非法的
endsequence

2. 对于or操作的情况，当且仅当一个局部变量流出每一个操作数序列的时候，这个局部变量才流出复合序列。如果局部变量在复合序列启动之前没有被赋值并且它仅在其中的一个操作数序列被赋值，那么它不会流出复合序列。
3. 一个匹配其操作数序列的or操作的一个操作数的每一个线程都作为一个独立的线程执行，并携带它自己的最新赋值到流出复合序列的局部变量。这些线程不必在局部变量上具有一致的计算结果。例如：

sequence s5;
    int x,y;
    ((a ##1 b, x = data, y = data1 ##1 c)
    or (d ##1 `true, x = data ##0 (e==x))) ##1 (y==data2);
    // 非法的，因为y没有在交集中
endsequence

sequence s6;
    int x,y;
    ((a ##1 b, x = data, y = data1 ##1 c)
    or (d ##1 `true, x = data ##0 (e==x))) ##1 (x==data2);
    // 合法的，因为x位于交集中
endsequence

4. 对于and和intersect操作的情况，从至少一个操作数流出的局部变量应该从复合序列流出，除非它被阻塞。如果下列条件中的一个条件成立，那么一个局部变量会被阻塞：
   1. 局部变量在复合序列的每一个操作数中或者从复合序列的每一个操作数流出时被赋值。或者，
   2. 局部变量被阻塞而不能从至少一个操作数序列中流出。

流出复合序列的一个局部变量的值是最后所赋的值。在复合序列的计算结束的时候两个操作数的线程被合并成一个。

sequence s7;
    int x,y;
    ((a ##1 b, x = data, y = data1 ##1 c)
    and (d ##1 `true, x = data ##0 (e==x))) ##1 (x==data2);
    // 非法的，因为x对于两个线程是共用的
endsequence

sequence s8;
    int x,y;
    ((a ##1 b, x = data, y = data1 ##1 c)
    or (d ##1 `true, x = data ##0 (e==x))) ##1 (y==data2);
    // legal since y is in the difference
endsequence