SVA用关键词sequence（序列）来表示设计中的逻辑事件。序列的基本语法是：
sequence name_of_sequence
<test expression>
endsequence
许多序列可以逻辑或者有序的组合起来生成更复杂的序列。SVA提供了一个关键词property（属性）来表示这些复杂的有序行为。属性的基本语法是：
property name_of_property
<test expression>；or
<complex sequence expressions>
endproperty
属性必须在模拟过程中被用于断言(assert)、假设(assume)或覆盖(cover)语句来发挥作用。
SVA提供了关键词assert来检查属性。其基本语法是：
assertion_name: assert property (property_name);
SVA提供了关键词assume来假设属性。其基本语法是：
assertion_name: assume property (property_name);
SVA提供了关键词cover来衡量协议覆盖。其基本语法是：
cover_name: cover property (property_name);
上图表明了SVA语言的基本构成。布尔表达式将设计中的信号组合起来，组成序列。然后序列逻辑或者有序的组合起来得到属性。最后通过关键词assert,cover和assume指示属性的具体作用。
2 蕴含操作符
上一小节中序列s2的失败由两个原因：(1)a为低电平；(2) a为高电平，b在两个cycle之后不为高电平。通常我们只关心第二种错误，第一种错误是一个无效的错误信息。因而我们希望通过定义某种约束技术，在检查的起始点无效时忽略这次检查。SVA提供了蕴含（Implication）实现这一目的。
蕴含的左边叫做先行算子(antecedent)，右边叫做后续算子 (consequent)。当先行算子成功时，后续算子才会被计算；如果先行算子不成功，那么整个属性被默认为“空成功”。另外要注意的是，蕴含只可用于属性定义中，不可用于序列中。
蕴含分为两类：
(1) 交叠蕴含（Overlapped implication）
用符号”|->”表示。如果先行算子匹配，在同一个时钟周期计算后续算子表达式。也可以加入固定延时”|-> ##2”，表示如果先行算子匹配，在两个时钟周期之后计算后续算子表达式。
(2) 非交叠蕴含（Non-overlapped implication）。
用符号”|=>”表示。如果先行算子匹配，在下一个时钟周期计算后续算子表达式。
利用蕴含，序列s2可以改为更符合我们需要的时序检查的属性p3：
property p3
@(posedge clk) a |-> ##2 b; // ##表示时钟周期延迟
end property
3 SVA检验器的时序窗口
上面讨论的延迟的例子都是固定的正延迟。延迟也可以用时序窗口的方式定义，从而给延迟限定一个范围。
例如：
(a&&b) |-> ##[1:3] c;
上述表达式实际上以下面三个线程展开：
(a&&b) |-> ##1 c或
(a&&b) |-> ##2 c或
(a&&b) |-> ##3 c
时序窗口可以用于属性以及序列。不同的是，第一个成功的线程将使整个属性成功，并结束这个属性；而序列可以有多个匹配都能使得序列成功，即第一个成功并不结束这个序列的检查，序列可以有多个成功的结束点。
时序窗口左边的值最小为0。时序窗口右边的值最大为$（它指示一个有限的但无边界的最大值）。检验器不停的检查表达式是否成功直到模拟结束。如果属性检查在模拟结束之前都没有成功，那么检查报告为“未完成的检验（incomplete check）”。如果序列在模拟结束之前检查没有结束，那么检查报告也为未完成的检验。
例如：
sequence s4;
@(posedge clk) a ##[1:3] b;
endsequence
property p4;
@(posedge clk) s4;
endproperty
Ø 大的时间窗口应该使用变量予以限定
当##[M:N]和[*M:N]运算符中的时间间隔很长（如大于20个时钟周期）时，编译或运行这样的运算符要占用很长的时间和很多的资源。
例如，带长时间间隔的非重叠事务：
a1:assert property(@(clk)start |-> ##[150:256] stop);
可改写位
logic [10:0] timer=0;
always @(posedge clk) begin:nooverlap
if(reset||stop) timer<=0;
else if(start) timer<=1;
else if(timer!=0 && timer<=255) timer<= timer + 1;
timing:assert property
disable iff(reset)
$rose(stop)||$rose(timer==256)
|-> ((timer>150) && (timer<=255))
)else …；
end:nooverlap
4序列操作符
1重复运算符
SVA语言提供三种不同的重复运算符：连续重复（consecutive repetition），跟随重复（go to repetition），非连续重复（non-consecutive repetition）。
连续重复
表明信号和序列将在指定数量的时钟周期内连续的匹配。信号的每次匹配之间都有一个时钟周期的隐藏延迟。连续重复的重复次数可以是一个窗口。
基本语法如下：
signal or sequence [*n] （n为表达式匹配的次数）
或者signal or sequence [*n:m] （表达式匹配的次数为n~m次）
例如：
property p5;
@(posedge clk) $rose(start) |-> ##2 (a[*3]) ##2 stop ##1 !stop;
endproperty
其中a[*3]可以被展开成：
a ##1 a ##1 a
跟随重复
表明信号将匹配指定次数，但不一定在连续的时钟周期上发生。跟随重复的主要要求是信号的最后一个重复匹配发生在整个序列匹配前的那个时钟周期。
跟随重复的基本语法如下：
signal [->n]
非连续重复
表明信号将匹配指定次数，但不一定在连续的时钟周期上发生。非连续重复不要求信号的最后一个重复匹配发生在整个序列匹配前的那个时钟周期。
非连续重复的基本语法如下：
signal [=n]
下面举例说明跟随重复和非连续重复的区别：
property p6;
@(posedge clk) $rose(start) |-> ##2 (a[->3]) ##1 stop ##1 !stop;
endproperty
property p7;
@(posedge clk) $rose(start) |-> ##2 (a[=3]) ##1 stop ##1 !stop;
endproperty
属性p6和p7做的检查为：在任何时钟上升沿start拉高后开始检查，两个时钟周期后，信号a连续或者间断的出现3次为高，接着信号stop在下一个时钟周期为高。p6与p7的唯一区别是，p6要求a第三次为高后的那个时钟周期stop必须为高，而p7只要求在a的第三个匹配之后，期望一个有效的信号stop，但不必在下一个时钟周期发生。
p6和p7都有一个未完成的检查，标记3s标出了检验器一个有效的开始，但在模拟结束前，a只重复为高两次，因而虽然信号stop出现了一次有效，但是模拟结束时这个检查未能完成。
2选择运算符
SVA允许在序列和属性中使用选择运算符。
例如
property p8;
@(posedge clk) c ? d==a : d==b ;
endproperty
在信号c为高时，检验d是否与a相等；在信号c为低时，检验d是否与b相等。
.3二元运算符
（1） and运算符
二进制运算符and可以用来逻辑地组合两个序列。当两个序列都成功时，检验才成功。两个序列必须具有相同的起始点，但是可以有不同的结束点。检验的成功点是后一个成功的序列的匹配点。
例如：
sequence s9a;
@(posedge clk) a ##[1:3] b;
endsequence
sequence s9b;
@(posedge clk) c ##[2:3] d;
endsequence
sequence s9c;
@(posedge clk) s9a and s9b;
endsequence
property p9;
@(posedge clk) s9a and s9b;
endproperty
一个有效的检验开始于时钟周期2。在时钟周期3时，s9a第一次成功，但必须等待s9b也成功，整个序列的组合才成功。在时钟周期4时，s9b第一次成功，因此s9c和p9都成功，并且p9结束，但s9c继续检查，在时钟周期5检验到另一个成功。
（2）intersect运算符
二进制运算符intersect与and很相似，但它还要求两个序列必须在相同时刻开始且结束于同一时刻。
（3）or运算符
二进制运算符or可以用来逻辑地组合两个序列。两个序列必须具有相同的起始点，但是可以有不同的结束点。只要其中一个序列成功，检验就成功。检验的成功点是前一个成功的序列的匹配点。
4 first_match 构造
使用了逻辑运算符（如and和or）的序列中如果指定了时间窗，就有可能出现同一个检验具有多个匹配的情况。first_match构造可以确保只用第一次序列匹配，而丢弃其他的匹配。这相当于在属性中定义这个相同的序列。
例如：
sequence s10a;
@(posedge clk) a ##[1:3] b;
endsequence
sequence s10b;
@(posedge clk) c ##[2:3] d;
endsequence
sequence s10c;
@(posedge clk) first_match(s10a or s10b);
endsequence
property p10;
@(posedge clk) s10a or s10b;
endproperty
序列s10c与属性p10做的是相同的检查，只保留s10a和s10b的第一次匹配。
5 throughout构造
throughout构造可以保证某些条件在整个序列的验证过程中一直为真，其基本语法如下：
(expression) throughout (sequence definition)
如果表达式没有在整个验证过程中保持为真，即使序列的其他检验都正确，也会导致整个检验失败。
6 within构造
within构造允许在一个序列中定义另一个序列。
其基本语法为：
seq1 within seq2
这表示seq1在seq2的开始到结束的范围内发生，且seq2的开始匹配点必须不晚于seq1的开始匹配点，seq2的结束匹配点必须不早于seq1的结束匹配点。
一个属性定义了设计的一个行为。一个属性可以作为一个假设、一个检查器或者一个覆盖率规范被用于验证。为了将这种行为用于验证，必须使用断言(assert)、假设（assume）或者覆盖(cover)语句。一个属性声明本身不会产生任何结果。
SVA中有七种类型的属性：
(1) sequence：由序列构成；
(2) negation：not property_expr；
(3) disjunction：property_expr1 or property_expr2；
(4) conjunction：property_expr1 and property_expr2；
(5) if…else：
if(expression_or_dist)
property_expr1
else
property_expr2
(6) implication：蕴含；
(7) instantiation：属性的实例可以被用作property_expr或者property_spec。
property_expr ::= sequence_expr | implication_expr
property_spec ::= [clocking_event] [disable iff( expression )] [ not ] property_expr
在序列、属性中都可以定义时钟。通常情况下， 在属性的定义中指定时钟，并保持序列独立于时钟是一种好的编码风格，这样可以提高序列的重用性。
SVA提供了关键词disable iff来实现检验器的复位，即某些条件为真时，我们不想执行检验。其基本语法如下：
disable iff (expression) <property definition>
disable iff只可用在属性中。
例如：
property p_dis;
@(posedge clk)
disable iff(reset) $rose(start) |=> a[=2] ##1 !start;
endproperty
SVA提供了下列系统函数来访问一个表达式的采样值。
(1) $rose(boolean expression or signal_name)：
当信号/表达式的最低位变成1时返回真。
(2) $fell(boolean expression or signal_name)：
当信号/表达式的最低位变成0时返回真。
(3) $stable(boolean expression or signal_name)：
当信号/表达式不发生变化时返回真。
(4) $past(signal_name, number of clock cycle,gating signal)：
得到信号在几个时钟周期之前的值。这个函数能够有效的验证设计到达当前时钟周期的状态所采用的通路是正确的。并且past可以由门控信号（gating signal）控制。
例如：property p_past;
@(posedge clk) (c&&d) |->($past((a&&b),2,e)==1’b1);
endproperty
当门控时钟e在任意给定的时钟上升沿有效时，检验如果表达式(c&&d) 为真，那么两个周期前，(a&&b)为真。
SVA还提供几个内建的函数来检查一些最常用的设计条件。
(1) $onehot(expression)：在任意给定的时钟沿，表达式只有一位为高。
(2) $onehot0(expression)：在任意给定的时钟沿，表达式只有一位为高或者没有任何位为高。
(3) $isunknown(expression)：在任意给定的时钟沿，表达式的任何位是否是x或者z。
(4) $onehot(expression)：在任意给定的时钟沿，计算向量中为高的位的数量。
2.8.1在序列和属性中使用形参
通过在序列中定义形参，相同的序列可以被重用到设计中具有相似行为的信号上。例如，我们可以定义下面的序列：
sequence s_lib1(a,b)
a||b;
endsequence
我们可以通过下面这个序列调用上面的序列：
sequence s_lib1_inst1
s_lib1(req1, req2);
endsequence
同样，与序列声明一样，一个属性在声明的时候可以带有可选的形式参数。当一个属性被实例化的时候，实参可以被传递到属性。通过使用实参替代形参，实参使得属性得到了扩展。例如，我们可以定义下面的属性：
property arb(a,b,c);
@(posedge clk) $fell(a) |-> ##1 (c&&d)[*4] ##1 b;
endproperty
下面三个断言都可以调用属性arb：
a1_1:assert property(arb(a1,b1,c1,d1));
a1_2:assert property(arb(a2,b2,c2,d2));
a1_3:assert property(arb(a3,b3,c3,d3));
2.8.2使用参数的SVA检验器（module）
SVA检验器模块中可以使用参数，这为创建可重用的检验器模块提供了很大的灵活性。
SVA检验模块如下：
Module generic_chk(input logic a,b,clk)
parameter delay=1;
property p1;
@(posedge clk) a |-> ##delay b;
endproperty
a1:assert property(p1);
endmodule
以下两个generic_chk的实例：
generic_chk #(.delay(2)) i1(a,b,clk); //将延迟参数改写为2个cycle
generic_chk i2 (c,d,clk); //使用默认的1个cycle
在序列或者属性的内部可以局部定义变量。局部变量能够在需要的时候在一个序列或者属性实例中动态地产生并能在序列结束的时候移除。变量的赋值接着子序列放置，用逗号隔开。
例如：
sequence s0;
int lvar;
@(posedge clk)
$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));
endsequence
序列在start拉高后开始有效的检查，序列中的局部变量lvar在每次enable匹配时，累加aa的值，并在序列结束匹配点处检查lvar是否与aout相等。
在上例中，局部变量在序列的实例中是不可见的。如果要使得子序列的局部变量可以被上层序列访问，必须声明一个局部变量并通过一个自变量传递到被实例化的子序列。
sequence s1(lvar);
@(posedge clk)
$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));
endsequence
sequence s2;
int v1;
c ##1 s1(v1) ##1 (do1 == v1);
endsequence
任务、任务线程、void函数、void函数线程以及系统任务（tasks, task methods, void functions, void function methods, and system tasks）可以在一个序列成功匹配的结束处调用。子程序调用，出现在紧跟着序列的以逗号分割的列表中。
举例说明：
sequence s1;
logic v, w;
(a, v = e) ##1
(b[->1], w = f, $display("b after a with v = %h, w = %h\n", v, w));
endsequence
在序列s1中定义了局部变量v和w，当a为高电平时，把向量e的值赋给v；然后b出现一次高电平时，把向量f的值赋给w，并调用系统任务进行打印。
任务、任务线程、void函数、void函数线程以及系统任务（tasks, task methods, void functions, void function methods, and system tasks）可以在一个序列成功匹配的结束处调用。子程序调用，出现在紧跟着序列的以逗号分割的列表中。
举例说明：
sequence s1;
logic v, w;
(a, v = e) ##1
(b[->1], w = f, $display("b after a with v = %h, w = %h\n", v, w));
endsequence
在序列s1中定义了局部变量v和w，当a为高电平时，把向量e的值赋给v；然后b出现一次高电平时，把向量f的值赋给w，并调用系统任务进行打印。
SVA中提供了两种方法将一个复杂序列分解成较为简单的子序列。一种方法是以序列的起始点作为同步点，另一种方法是以序列的结束点作为同步点。后一种方法通过为序列名字追加上关键词ended来表示。
举例说明：
sequence s0;
@(posedge clk) a ##1 b;
endsequence
sequence s1;
@(posedge clk) c ##1 d;
endsequence
property p0;
s0 |=>s1;
endproperty
property p1;
s0.ended |-> ##2 s1.ended;
endproperty
属性p0和p1做的是相同的检查。p0是以序列的起始点作为同步点，序列s1从s0匹配后的一个时钟周期开始检验；p1是以序列的结束点作为同步点，序列s1的结束匹配时间必须在s0的结束匹配时间之后的2个时钟周期。
使用ture表达式，可以在时间上延长SVA检验器，能够使得序列的结束点延长一个时钟周期。这可以用来实现同时监视多个属性且需要同时成功的复杂协议。
例如：
sequence s0;
@(posedge clk) a ##1 b;
endsequence
sequence s0_ext;
@(posedge clk) a ##1 b ##1 ‘true;
endsequence
sequence s1;
@(posedge clk) c ##1 d;
endsequence
property p0;
@(posedge clk) s0.ended |-> ##2 s1.ended;
endproperty
property p1;
@(posedge clk) s0_ext.ended |=> s1.ended;
endproperty
属性p0和p1做的是相同的检查。序列s0_ext的成功匹配点比s0往后移了一个时钟周期。因此属性p0检查s0与s1成功匹配点是否相隔两个时钟周期，属性p1检查s0_ext与s1成功匹配点是否相隔一个时钟周期。
SVA允许序列或者属性使用多个时钟定义来采样独立的信号或者子序列。
2.13.1多时钟序列
多时钟序列由单时钟序列通过延迟连接符号##1连接而成。连接符号##1是非交叠的，并且能够同步不同子序列的时钟域。它表示从第一个单时钟序列的结束点，到第二个单时钟序列的起始点。当一个序列中使用了多个时钟信号时，只允许使用##1延迟构造。
例如：
sequence s_mul_clk;
@(posedge clk1) a ##1 @(posedge clk2) b;
endsequence
序列s_mul_clk做的检查是：当信号a在时钟clk1的任意给定上升沿为高时，序列开始匹配，接着查找clk2的最近的上升沿，检查b是否为高。clk1的时钟周期3开始第一次有效的检查，查找clk2的最近的上升沿为其时钟周期2，检测到b为高，检查成功；clk1的时钟周期7开始第二次有效的检查，查找clk2的最近的上升沿为其时钟周期3，检测到b为低，检查失败。
多时钟序列只能用延迟连接符号##1连接单时钟序列。注意的是以下的序列都是非法的：
@(posedge clk1) s1 ##0 @(posedge clk2) s2
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2
2.13.2多时钟属性
多时钟属性的检查规则和多时钟序列相同。多时钟属性除了使用延迟连接符号##1，还可以对单时钟序列使用非交叠蕴含运算符。要注意的是，并不是不允许在多时钟序列中使用交叠蕴含运算符，只是不允许将其连接两个时钟定义不同的单时钟序列。例如，下面的语句就是合法的：
@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk1) s2
多时钟属性也可以使用逻辑运算符（and,or,not）连接两个单时钟序列。
2.13.3 matched构造
如果一个序列中定义了多个时钟，构造matched可以用来监测子序列的结束点。
例如：
sequence e1;
@(posedge clk1) (a ##1 b ##1 c) ;
endsequence
sequence e2;
@(posedge clk2) start ##1 e1.matched ##1 stop;
endsequence
信号start在clk2的时钟周期2为高，然后我们检测到序列e1在clk2的时钟周期3出现一次匹配，并且在clk2的时钟周期4信号stop为高，因此在clk2的时钟周期4出现序列e2的第一次成功；clk2的时钟周期5开始第二次有效的检验，但是在clk2的时钟周期6我们没有检测到序列e1的成功匹配点，因此在clk2的时钟周期6出现序列e2的失败。
理解matched构造的使用方法的关键在于，被采样到的匹配的值一直被保存到另一个序列最近的下一个时钟边沿。
SVA提供了关键词assert来检查属性，assert语句的基本语法是：
assertion_name: assert property(property_name);
执行块可以在属性成功或者失败后执行某些语句。
执行块的基本语法如下：
assertion_name:
assert property (property_name)
<success message>;
else
<fail message>;
执行块可以用来显示成功和失败。
有两种方法可以将SVA检验器连接到设计中：
（1） 在模块定义中内建或者内联检验器。
（2） 将检验器模块与模块、模块的实例或者一个模块的多个实例绑定。
检验器模块用来检验一组通用的信号，检验器可以与设计中任何的模块或者实例绑定。定义独立的检验器模块，增强了检验器的可重用性。
绑定的语法如下：
bind <module_name or instance_name>
<checker name> <checker instance name>
<design signals>;
举例说明绑定的使用：
下面为检验器模块的代码：
module mutex_chk(a,b,clk)
logic a,b,clk;
property p1;
@(posedge clk) not(a&&b);
endproperty
endmodule
有如下所示的顶层模块：
module top(..);
inline u1(clk,a,b,in1,in2,ou1);
inline u2(clk,c,d,in3,in4,ou2);
endmodule
绑定的语句如下：
bind top.u1 mutex_chk i1(a,b,clk);
bind top.u2 mutex_chk i1(c,d,clk);
功能覆盖分为两类：对属性的覆盖和对序列的覆盖。
对属性覆盖的cover语句的结果包含下面的信息：
(1) 属性被尝试检验的次数
(2) 属性成功的次数
(3) 属性失败的次数
(4) 属性空成功的次数（由于使用蕴含）
例如得到如下的属性覆盖报告：
c0, 596 attempts, 202 match, 51 vacuous match（真正成功的次数为match的次数减去vacuous match的次数）
对序列覆盖的cover语句的结果包含下面的信息：
(1) 序列被尝试检验的次数（attemps）
(2) 所有成功的次数（total match）
(3) 初次成功的次数（first match）
(4) 序列空成功的次数（vacuous match）（总是为0，因为序列中不允许使用蕴含）
例如得到如下的序列覆盖报告：
c1, 596 attempts, 361 total match, 151 fisrt match, 0 vacuous match
序列中如果指定了时间窗，就有可能出现同一个检验具有多个匹配的情况。total match就包括了所有的成功，而first match只包括检验的第一次匹配。
SVA提供了关键词cover来衡量协议覆盖。其基本语法是：
cover_name: cover property (property_name or sequence_name);
通过运用cover语句我们可以得到属性或者序列的执行情况。我们可以把我们希望发生的情景表达成属性或者序列，并通过检测所有属性或者序列的检验至少真正成功一次，来实现功能覆盖。利用与assert语句中一样的执行块，我们可以控制模拟环境和收集功能覆盖数据。
下面以一个请求情景（Request Scenario）为例。
在任何给定的时间，有三个主控设备可以请求访问总线。这就意味着主控设备的req信号有七种可能的组合（0表示主控设备正在请求总线）。
测试平台应该生成上表中所有的输入组合。
七个属性定义了上表中的所有可能的请求组合。每个属性都与cover语句相连。我们期望每个请求组合都出现三次，因此我们只要检测七个属性是否都被成功检测到三次。并且，我们可以利用flag标志位来控制模拟环境，例如所有组合都检测到三次后就终止模拟。
要注意的是，每次属性或者序列的匹配都会执行action block在中的语句，如果在某一时钟周期同时产生了多个匹配，那么这个语句就会相应的被执行多次。
在形式验证和动态仿真中，assume语句将属性指定为环境中的假设。当一个属性被假设，工具会约束环境使得属性的检验得到满足。
在形式验证中，被假设的属性不会被强制满足检验。被假设的属性可以认为是被断言的属性的前提假设（hypothesis）。
在动态仿真中，环境必须被约束使得被假设的属性满足检验。和被断言的属性一样，被假设的属性也要被检查，并且在失败时报错。
举例说明assume语句的使用：
检查信号req的属性如下：
property pr1;
@(posedge clk) !reset_n |-> !req; //when reset_n is asserted (0),keep req 0
endproperty
property pr2;
@(posedge clk) ack |=> !req; // one cycle after ack, req must be deasserted
endproperty
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack;
// hold req asserted until and including ack asserted
endproperty
检查信号ack的属性如下：
property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
property pa2;
@(posedge clk) ack |=> !ack;
endproperty
在假设断言a1, assume_req1,assume_req2, and assume_req3一直满足的前提下，检查断言assert_ack1和assert_ack2是否满足检验。
a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
assume_req1:assume property (pr1);
assume_req2:assume property (pr2);
assume_req3:assume property (pr3);
assert_ack1:assert property (pa1)
else $display("\n ack asserted while req is still deasserted");
assert_ack2:assert property (pa2)
else $display("\n ack is extended over more than one cycle");
要注意的是assume语句不能使用执行块，因为执行语句对于假设来说没有意义。
SVA支持expect构造，它等待属性的成功检验，并将except构造后面的代码作为一个阻塞的语句来执行。expect语句允许在一个属性成功或者失败后使用一个执行块。
举例说明：
program tst;
initial begin
# 200ms;
expect( @(posedge clk) a ##1 b ##1 c ) else $error( "expect failed" );
ABC ...
end
endprogram
上例中，在expect语句失败后打印失败信息，并且语句ABC要等待expect语句检验成功或者失败后才执行。
