systemverilog断言简介 形式验证 第3章

   目录

一、基本断言概念

1、一个简单的仲裁器示例

2、什么是断言（assertion）

3、什么是假设（assumption）

4、什么是覆盖点（cover point）

5、对断言语句的阐述

6、SVA断言语言基础知识

二、即时断言

1、写即时断言

2、过程代码的复杂性和断言FINAL的动机

3、程序块中的位置

4、布尔构建块

 5、并发断言基础知识和计时

6、采样和断言计时

7、采样值函数

8、并发断言时钟边沿

9、并发断言重置（禁用）条件

10、设置默认时钟并复位

三、序列、属性和并发断言

1、序列语法和示例

2、属性语法和示例

3、命名序列和属性

4、断言和隐式多线程

5、写入属性

1）在规格阶段规划属性

2）RTL开发期间的嵌入式属性

3）以验证为中心的属性

4）将属性与设计联系起来

         为了利用形式验证（FV）的能力来证明设计的正确性，必须首先有一种方法来表达设计正确意味着什么。最流行的方法是通过断言中指定的属性(property)，使用SystemVerilog断言（SVA）语言。

        尽管工业界和学术界有许多specification方法，例如在第1章中简要提到的属性规范语言（PSL）语言和开放验证库（OVL）断言库，但在过去十年中，SVA已有效地成为指定寄存器传输级（RTL）断言的工业标准。

        在详细探讨FV技术之前，需要先学习SVA语言。本章中的内容是要求读者已经熟悉SystemVerilog建模语言。

        本章将重点放在与FV最相关的断言构造上，SVA断言在仿真环境中也非常有用。

        如果想了解完整的语法定义、每个可用的语言特性或其他细节，有一些完全基于SVA的优秀长篇书籍：Ben Cohen, Srinivasan Venkataramanan, Ajeetha Kumari, and Lisa Piper, SystemVerilog Assertions Handbook, 3rd Edition with IEEE 1800-2012, VhdlCohen Publications, 2013和 Eduard Cerny, Surrendra Dudani, John Havlicek, and Dmitry Korchemny, SVA: The Power of Assertions in SystemVerilog, 2nd Edition, Springer, 2014。

        但本章中的内容也足以高效地使用SVA断言。

        在本章中，将描述SystemVerilog语言参考手册（LRM）IEEE标准1800-2012中描述的SVA语言。本章后面的描述中，把该文档简称为LRM。

一、基本断言概念

        本章使用一个具体的目标模型来描述SVA断言的概念和用法。

1、一个简单的仲裁器示例

        使用的模型是一个简单的仲裁器设计，如图3.1所示

         这是一个仲裁器，有四个请求代理，每个代理都能够使用一位req信号请求共享资源。gnt信号指示哪个代理当前被授权使用该资源。还有一个opcode输入，允许某些命令覆盖仲裁器的正常行为，例如强制特定代理获得优先级，或在一段时间内切断对资源的所有访问。

        还有一个error输出，表示发送了错误的操作码或非法的操作码序列。实现此设计的top级System Verilog（SV）模块的接口代码如下所示：

typedef enum logic[2:0] {NOP,FORCE0,FORCE1,FORCE2,
FORCE3,ACCESS_OFF,ACCESS_ON} t_opcode;
module arbiter(
input logic [3:0] req,
input t_opcode opcode,
input logic clk, rst,
output logic [3:0] gnt,
output logic op_error
);

2、什么是断言（assertion）

        最基本的，断言是设计的陈述，希望它始终是对的。在这个仲裁器的例子中，一个简单的例子可能是：当代理0未被请求时，永远不会授权给它。

check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant
without request for agent 0!”);

        正如下面的讨论中看到的，断言可能比上面的简单布尔表达式复杂得多，涉及逻辑含义以及值随时间变化的潜在陈述。

        在模型上运行仿真时，当仿真器检测到代码中的任何SVA断言都不正确时，通常会标记一个错误。

        上面的示例中，如果在仿真中看到gnt[0]==1和req[0]== 0，则将显示消息"Grant without request for agent 0！"。

        当运行形式属性验证（FPV）工具时，断言被视为证明目标：从数学上证明RTL模型永远不会违反此断言。

        在深入研究技术细节之前，还应该了解另外两种类型的财产：assumptions and cover points。

3、什么是假设（assumption）

        假设与断言类似，但假设通常指定用于表示验证环境约束的条件，而不是指定被测设备的行为。由于输入或其他环境因素，这些通常是外部保证为真的条件。例如，希望仲裁器只能看到合法的非NOP操作码到达其操作码输入端：

good_opcode: assume property (opcode inside {FORCE0,FORCE1,FORCE2,
FORCE3,ACCESS_OFF,ACCESS_ON}) else $error(“Illegal opcode.”);

        在仿真中，假设的处理方式与断言完全相同：仿真器检查当前仿真值是否违反了指定的条件，如果不违反，则标记违规并打印消息。但这在概念上的含义与断言失败仍然有些不同：失败的假设通常意味着测试环境、测试台（testbench）代码或相邻的设计模块中有问题，而失败的断言通常表示测试中的设计存在问题。（这并不是严格要求，因为假设内部设计节点是合法的，在以后的章节中详细讨论这种情况。）在上面的示例good_opcode中，这表明测试台错误地将非法操作码驱动到设计中。

        在FV中，假设和断言之间有一个主要区别。假设是工具假设为真的东西，假设被视为条件，用于证明断言的真实性。没有假设时，FV工具允许任何可能的值输入到正在分析的模型中，假设是用户将这些值引导到允许行为的主要方法。在大多数情况下，为了消除对不现实行为的考虑并正确证明设计中的断言，需要一组好的假设。

4、什么是覆盖点（cover point）

        SVA覆盖点的指定方式与断言和假设类似，但其含义有所不同。断言或假设总是正确的，覆盖点只是偶尔正确的：指定了某种有趣的条件，确保正在测试。例如，在上面的仲裁器中，可能希望确保正在测试所有代理同时请求资源的可能：

cover_all_at_once: cover property
(req[0]&&req[1]&&req[2]&&req[3]);

        在仿真中，大多数用户都会集体检查覆盖点：每当覆盖点被击中时，工具或脚本都会将信息保存到数据库中，最终用户可以在运行测试套件中的所有仿真测试后检查总覆盖率。通常希望确保每个覆盖点至少命中一次；如果没有，这将揭示测试中的潜在漏洞。

        在FV中，覆盖点也起着重要作用。尽管FV理论上涵盖了系统的所有可能行为，但用户可以指定限制可能的假设或其他输入要求。这会导致过约束：可能会意外地指定一些假设，以排除系统中有趣的取值。确保FPV环境能够达到所有覆盖点是FV的关键步骤。

5、对断言语句的阐述

       断言、假设和覆盖点都是用SVA中基本相同的机制指定的。因此大多数定义它们的机制对于这三种类型的构造都是相同的。断言陈述（此处使用的方式与LRM[IEE12]中定义的方式相同）可以等同地指断言、假设或覆盖点。

6、SVA断言语言基础知识

        SVA断言语言可以看作是复杂度不断增加的几层，如图3.2所示。

•  布尔值是标准的SystemVerilog布尔表达式。布尔表达式可以是单个逻辑变量或公式，例如上述覆盖点示例中的（req[0]&&req[1]&&req[2]&&req[3]）。
• 序列是关于布尔值（或其他序列）随时间发生的陈述。依赖于明确定义的计时事件来定义时间流逝。例如，以下序列表示两个时钟周期中的一个请求和一个授权：

req[0] ##2 gnt[0]

• 属性将序列与其他操作符结合在一起，显示蕴含和相似的概念，以表达设计中预期保持的一些行为。例如，如果在两个周期后收到一个请求，然后是一个授权，这意味着授权将在下一个周期取消断言：

req[0] ##2 gnt[0] |-> ##1 !gnt[0]

• 断言语句是使用assert、assume、cover关键字之一的语句，导致SVA属性被检查为断言、假设和覆盖点。需要在某种断言语句中使用属性，否则属性无效。例如，检查上述属性的断言语句为：

gnt_falls: assert property(req[0] ##2 gnt[0] |->
##1 !gnt[0]);

       接下来会更详细地讨论序列、属性和断言语句，但在这之前，还有一个关键概念需要引入：即时断言（immediate）和并发（ concurrent）断言：

• 即时断言语句是简单的断言语句，在过程代码中访问它们时都会检查该断言语句；只允许布尔参数，没有时钟或复位机制，也不支持许多高级属性运算符。因此无法检查随时间变化的情况。在SVA中，立即断言由不带关键字" property"的断言表示，如：

imm1: assert (!(gnt[0] && !req[0]))

• 并发断言语句总是相对于一个或多个时钟进行评估，可以描述跨越时间的行为，并允许许多其他运算符支持有关时间间隔内逻辑含义的高级语句，比直接断言语句用得多。在SVA中，并发断言通过在断言中包含关键字" property"来表示，如：

conc1: assert property (!(gnt[0] && !req[0]))

        虽然并发断言conc1看起来类似于即时断言imm1，但它们的求值有一些重要的区别。在过程代码中访问即时断言时，它会被求值，而并发断言只在定义良好的时钟边缘求值。

二、即时断言

        即时断言是最简单的断言语句，通常被视为SystemVerilog过程代码的一部分，并且在代码评估期间每当访问它们时都会进行评估。没有时钟或复位的概念（除了可能控制其封闭程序块的任何时钟/复位），因此无法验证跨越时间的行为；还容易受到SystemVerilog过程代码的常见危害：“时间增量”问题，由于对过程（always或always_*）块进行多次求值，可能会受到时间步长临时值的影响。

        通常能使用并发断言就不使用即时断言。这项建议有几个原因：

• 使用与已知时钟相关的断言（并发断言直接支持的特性），有助于保持预期行为的清晰和充分理解。
• 时间增量危险，即时断言可能记录在时间步结束时更改的临时值，而导致无效的故障报告，并使调试更加困难。
• 除非即时断言位于计时程序块中，否则与始终不相关，因此模型或测试台计时行为的变化可能会产生不可预测的结果。

        但在某些情况下需要即时断言：

• 在函数或无时钟的结构中：希望在函数中添加立即断言；例如检查其参数的安全性或检查计算。
• 对于形式等价验证（FEV）工具：在第8章中，状态匹配FEV工具将逻辑分解为组合逻辑锥，许多工具只能处理用于证明等价性的无时钟假设。

        必须谨慎使用，仅在上述情况下才建议使用即时断言。

1、写即时断言

        建议用户使用立即断言的变体，最终延迟即时断言（final deferred immediate assertions）。最终延迟即时断言语句描述起来相对简单：只需使用assert final后跟任何布尔表达式，前面带有可选标签，后面带有失败消息。（如果使用的是尚未采用最新LRM的电子设计自动化（EDA）工具，则可能需要使用观察到的延迟即时断（observed deferred immediate assertion） assert #0，这在大多数常见情况下表现相同。有关这些结构的更多详细信息，请参见LRM第16.4条。）

        如果想编写一个即时断言，在代理0未请求访问时，没有授予它访问权限，可以编写以下语句：

grant0_ok: assert final (!(gnt[0] && !req[0])) else
$error(“Grant without request for agent 0.”);

        标签grant0_ok是断言的可选名称；如果没有标签，大多数EDA工具将自动生成名称，但建议自己命名一个。

        操作块else$error...也是可选的，如果断言失败不存在，大多数仿真工具都会为断言失败生成默认消息。建议写一些有意义的内容，以帮助仿真调试。

        这个断言可以放在gnt和req信号可见的任何模块中的always块内，或者放在可以访问这些信号的函数内。也可以将其放置在模块内的一个always块之外；在本例中，它被视为隐式always_comb块，每次执行其过程代码时，都会检查断言。

2、过程代码的复杂性和断言FINAL的动机

        在SystemVerilog中执行过程代码（主要是always块）的方式可能会让许多用户感到惊讶，甚至有些用户已经用这种语言设计了多年。需要记住三个关键概念：

• 在一个always块中，语句按照它们出现的顺序执行，就像软件代码一样。
• 多个always块没有确定的执行排序；可以按任何顺序执行。
• 如果always块的敏感列表中的信号发生变化（由于执行另一个always块或其他类型的赋值），则在同一时间步中再次执行。

        这些可能会导致一些即时断言的行为，会让用户在不熟悉LRM的情况下感到惊讶，所以该语言的最新版本引入了延迟断言的概念。这是一种遵循特殊规则的即时断言形式：如果在单个仿真时间步中多次执行它们所在的过程，则只报告最终执行的结果。

        为了更清楚地说明这一点，这里有一个RTL代码片段编写得非常糟糕的例子，它使用了非延迟即时断言：

always_comb begin : add_1_to_evens
if (f_even(i) && i < 9) begin
i = i + 1;
a1: assert (i >= 10) else $error(“i is %0d”,i);
end
end
always_comb begin : add_1_to_odds
if (f_odd(i) && i < 10) begin
i = i + 1;
a2: assert (i >= 10) else $error(“i is %0d”,i);
end
end

        假设f_even正确地为偶数返回true，f_odd正确地为奇数返回true，如果在某个地方被分配了一个小于10的值，则上面的一对always块将反复执行，每次交替地将i增加1，每次i增加但尚未达到最大值时都会看到断言失败：

Assertion failure in myfile.v:40: i is 4
Assertion failure in myfile.v:34: i is 5
Assertion failure in myfile.v:40: i is 6
Assertion failure in myfile.v:34: i is 7
Assertion failure in myfile.v:40: i is 8
Assertion failure in myfile.v:34: i is 9

        用户会发现上面的消息非常令人困惑，因为在仿真器的任何时间步结束时，会看到 i 总是至少为10。在时间步中更改的中间值触发了这些断言。这就是为什么引入了延迟断言：对于延迟断言，在任何仿真时间步中，只报告给定过程中每个断言的最终执行结果。

        在上面的例子中，如果每个断言都被一个assert final替换，那么将不会看到任何违规行为：在任何给定时间步的每个过程最后执行时，要么 i 具有合法值，要么不再检查断言。

       建议无论何时使用立即断言，都使用延迟断言。

3、程序块中的位置

        即时断言还有一个复杂之处，在执行其行时对其变量保持的任何值进行操作；这与程序结束时信号确定的值不同。下面是一个带有放置不当的即时断言的过程的示例：

always_comb begin
gnt = 4’b0;
no_conflict: assert final ($onehot0(gnt));
if (|req)
gnt = f_compute_grant (req);
end

        在本例中，编写断言no_conflict是为了检查是否始终最多只有一个授权。但是因为它被放置在f_compute_grant调用之前，所以它实际上永远不会检测到故障，即使f_compute _grant函数中存在错误：在到达断言行时，gnt的值将始终是之前在该行上分配的0。以下版本更有意义：

always_comb begin
gnt = 4’b0;
if (|req)
gnt = f_compute_grant (req);
no_conflict: assert final ($onehot0(gnt));
end

        需要注意：立即断言的final修饰符仅表示在每个时间步中使用其封闭always块的最终执行；并不表示它检测到其变量的最终值。

4、布尔构建块

        在结束对即时断言的讨论之前，应该检查SystemVerilog语言提供的各种布尔构建块，这些不是严格意义上的断言，而是有用的速记，可以为常见情况编写更清晰、更简洁的断言。

        它们特别有用，可以应用于即时断言和并发断言。在大多数情况下，它们的含义相对来说是不言自明的，因此不在这里详细解释它们，只提供表3.1来总结在断言上下文中最有用的结构：

 5、并发断言基础知识和计时

        正如在上一节中所讨论的，为FPV编写的大多数断言都是并发断言。这些断言支持时钟和复位的明确规范，并且能够检查值随时间的行为。在讨论更复杂的序列和属性概念之前，在简单布尔表达式上引入并发断言，这样可以讨论它们的计时工作原理。

        下面是一个并发断言的示例，用于检查在时钟clk外部复位的任何上升沿，有一个可接受的非NOP操作码：

safe_opcode: assert property (
@(posedge clk)
disable iff (rst)
(opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))
else $error(“Illegal opcode.”);

        从这个例子中，可以看到并发断言的语法与即时断言有几个明显的不同：

• 断言语句用关键字assert property声明。
• 包含一个可选的时钟边缘。
• 有一个可选的复位规范，使用关键字disable-iff。

        并发断言可以定义自己的时钟和复位，所以并发断言通常最有意义的做法是使用外部过程代码，而不是always块。也可以将它们包含在过程代码中，但还是建议避免使用这种用法，因为它会在断言和过程计时之间引入复杂的关系。（如果想了解此用法的详细信息，请参阅LRM第16.14.6节。）

6、采样和断言计时

        并发断言对其参数的采样值进行操作，本质上在任何仿真时间步（time step），每个变量的采样值都是该变量在上一仿真时间步结束时获得的值。

        在图3.3中，看到了一个信号sig1，其值在不同的时间发生变化，以及一个并发断言：

sig1_off: assert property (@(posedge clk1) !sig1);

     断言结果在时钟的每个正边缘计算，它们总是检查在前一时间步骤结束时采样的值。因此结果表明：

• 在阶段4，sig1刚刚变为0，但在clk1的上升沿之前为1，因此断言失败。
• 在阶段6，sig1刚刚变为1，但在clk1的上升沿之前为0，因此断言成功。
• 在阶段8，sig1在时钟边缘之前和之后都是1，因此断言失败。
• 在第10阶段，sig1在时钟上升沿之前的很长时间内变为0，因此断言成功。

        只要采样规则对于并发断言中使用的所有值都是一致的，那么由其逻辑定义的任何failure都应该如预期的那样，只要failure值在相关时钟的边缘之前是可见的。

        许多EDA工具在其输出中补偿了这种固有的一对一行为，因此使用的特定工具可能会或可能不会以这种方式在信号转换后报告failure。但如果它们符合语言规则，将始终使用这些采样值来计算断言结果。

        如果在过程代码中放置并发断言，或者包含使用非时钟元素的术语（如软件调用），并创建采样值和非采样值可能合并在一个断言中的情况，会导致麻烦。这是将并发断言放在过程代码之外的另一个原因。

7、采样值函数

        SVA提供了一组采样值函数，与并发断言相同的方式对采样值进行操作的内置函数。例如，如果用户希望确保只要没有授权，上一个周期就没有请求。可以这样写断言：

no_grant_ok: assert property (@(posedge clk)
(|gnt) || !$past(|req));

        此断言检查所需的条件，req和gnt值都在clk的正边缘之前采样，$past函数在一个周期之前检查其参数的值。这些函数都继承断言语句、序列或属性的时钟，尽管它们也可以传递显式时钟参数。

        表3.2显示了最有用的采样值函数及其摘要和使用示例。（这里显示了最常用的简单表单：有关详细信息和全套选项，请参阅LRM第16.9.3节。）

        使用这些函数时需要注意：X或Z值的问题。许多仿真器支持包含这些值的4值（0、1、x、z）运行，这一特性已添加到一些FV工具中。

        根据LRM，从X到1的转变视为$rose，而从X到0则视为$fell。如果用户的目标是一个允许这些值的验证环境，并且不希望从X/Z转换为上升或下降，那么可能应该使用序列符号，如下一节所述，而不是这些简易函数。

8、并发断言时钟边沿

        创建并发断言时，时钟是一个重要的考虑因素。该时钟用时钟标识符表示，例如@（posedge clk1）。时钟表达式决定对哪些值进行采样，如果使用了错误的时钟，会产生意外的行为。一个常见的错误是省略一个边并使用像@(clk1)这样的表达式：这使得断言作用于正、负时钟边缘，会检查每个相位而不是每个周期。

        如果是基于锁存器的设计，这有时可能是真正的用户意图，但更常见的是，确实需要指明边缘。如果将慢时钟传递给断言，它可能会忽略仅持续较快时钟的一个阶段的短期值。

        如果使用了$past等采样值函数，或者使用了序列延迟（将在下一节中描述），选择不同的时钟实际上可以改变计数的周期数。

        在图3.4中，可以看到具有相同逻辑表达式的断言，因传入的时钟不同而产生不同行为。

check_posedge: assert property (@(posedge clk1) !sig1);
check_anyedge: assert property (@(clk1) !sig1);
check_posedge4: assert property (@(posedge clk4) !sig1);

         可以看到：

• 在阶段4，check_posedge和check_anydge断言检测到sig1的零值，但是check_posedge4 断言没有检测到，因为还没有clk4的正边缘。
• 在阶段7，check_anyedge断言检测到sig1的一个相位毛刺，但其他两个都没有检测到，因为该脉冲不会持续到任何正时钟边缘。
• 在阶段14，三个断言都通过，因为sig1在两个时钟的正边缘之前的值都为0。

        总结：应该确保了解用于断言的时钟以及原因。想检测一个相位的“failure”值，还是忽略它们？想寻找与最快的时钟相关的每一个变化，还是真的只关心一些用来感知输出的较慢的时钟？

9、并发断言重置（禁用）条件

        除了时钟，并发断言还允许用户使用disable-iff指定复位条件。目标是在复位期间关闭断言检查：复位时，可以允许设计中有一定程度的任意“垃圾”值，并且用户可能不想处理由于这些任意值而导致的无效断言失败的干扰。

        断言复位是同步的，只要满足禁用条件，断言就会立即关闭。

        不要试图在disable子句中插入各种逻辑：因为这与断言的其余部分的时间不同，可能会得到令人困惑的意外结果。

        例如，考虑以下两个断言，这两个断言都试图说明在复位之外，如果至少有一个授权，那么应该有一个请求：

bad_assert: assert property (@(posedge clk)
disable iff
(real_rst || ($countones(gnt) == 0))
($countones(req) > 0));
good_assert: assert property (@(posedge clk)
disable iff (real_rst)
(($countones(req) > 0) ||
($countones(gnt) == 0)));

        乍一看，这些可能在逻辑上是等价的：这两个断言都表示用户必须没有任何授权，或者必须至少有一个当前较高的请求。但由于bad_assert将gnt信号置于禁用状态（未采样），实际上会比req值早一个周期查看gnt值，从而导致图3.5所示波形上的故障。

         在图3.5中，第6阶段显然存在一个问题，即没有请求的授权。断言good_assert将使用clk1的上升沿之前的采样值在第8阶段报告此失败。

        断言bad_assert在除6之外的每个阶段都被禁用。就在第8阶段上升沿之前的采样值显示|req false，但gnt的当前值（由于disable子句而不是采样值）禁用此断言的检查。

注意：在SVA断言的复位（disable iff）中，仅使用实际复位，在全局范围内长时间关闭模型主要部分的信号。由于异步行为，在复位项中使用杂项逻辑可能会产生令人困惑的结果。

10、设置默认时钟并复位

        当结束对并发断言的SVA计时和复位的检查时，还有一个更重要的语言特性需要讨论。

        到目前为止，指定断言的时钟和复位可能有点冗长：

good_assert: assert property @(posedge clk)
disable iff (rst)
(|req || !(|gnt)) else $error(“Bad gnt.”);
safe_opcode: assert property (
@(posedge clk)
disable iff (rst)
(opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))
else $error(“Illegal opcode.”);

        SVA提供了一种为模块中的并发断言设置全局时钟和复位的方法，可以编写一次并覆盖多个断言。使用default clocking语句声明默认时钟，使用default disable iff 语句声明默认复位。

        如果声明了这些默认值，它们将应用于当前模块中的所有断言语句，但显式包含不同时钟或复位的断言语句除外。

        以下代码相当于上面的两个断言：

default clocking @(posedge clk); endclocking//声明了全局时钟
default disable iff (rst);//声明了全局复位

good_assert: assert property
(|req || !(|gnt)) else $error(“Bad gnt.”);

safe_opcode: assert property (
(opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))
else $error(“Illegal opcode.”);

        上面的default clocking和default disable iff 语句之间的不对称语法并不是错误：default clocking需要endclocking，而default disable iff 不需要。

        一般许多使用相同时钟和复位的断言，在模块中声明这些默认值可以显著提高断言代码的可读性，也可以防止误用时钟和复位。

        在这描述了这些默认结构的用法，本章和后续章节中的编码示例通常不会为每个断言指定显式时钟和复位。

三、序列、属性和并发断言

        并发断言能够声明随时间发生的行为，并使用语言的多层来构建复杂序列和属性。

1、序列语法和示例

        序列是一段时间内出现的一组值的规范，用于构建序列的基本操作是延迟标识符。格式为##n（针对特定数量的时钟）或 ##[a:b]（表示a和b时钟之间的可变延迟）。特殊符号$ 表示潜在的无限循环数。当一个序列的指定值全部出现时，该序列被称为匹配。 

        具有可变延迟的序列在任何执行跟踪期间可能具有多个重叠匹配。图3.6显示了几个简单序列的示例。

         另一个常见的序列操作是重复运算符[*m:n]，这表示子序列要重复一定次数。同样上限可能是$，表示重复次数可能不受限制。图3.7显示了使用该运算符的一些示例。

         序列可以使用 and 或 or 运算符进行逻辑组合。（注意它们不同于SystemVerilog的 || 和 &&运算符，后者为布尔表达式提供逻辑and或or。）

        当使用 and 运算符时，表示两个序列同时开始，尽管它们的端点可能不匹配。对于 or 运算符，两个序列中的一个必须匹配。

        throughout 运算符也很有用，检查某个布尔表达式在序列的整个执行过程中是否保持为真；

a throughout (!c[->2]);
// 在整个!c[->2]验证期间，a一直为真

         within 运算符检查一个序列在另一个序列的执行过程中发生。

a within b;
//a在b的开始到结束的时间范围内发生。

        最后一组常用的序列运算符是 goto 重复运算符[->n]和[=n]，这表明某个值在序列中正好出现n次，这些出现可能是非连续的，其间具有任意的其他活动。

       跟随重复运算符 [->n] 在值的最后一次出现时匹配，如下：

a |-> b[->3] ##1 c;
//!a a b !b !b b !b b c 这个可以匹配

//!a a b !b !b b !b b ！b c 这个不匹配

        非连续重复运算符 [=n] 允许在最后一次发生后有任意数量的额外时间，如下：

a -> b[->3] ##1 c;
//!a a b !b !b b !b b ！b c 这个可以匹配，对最后一次出现的b值没有限制

         上面的简单示例在技术上是代码片段，而不是有用的语句。

        序列对于构建覆盖属性非常有用，下面是一些在仲裁器示例中可能有用的cover断言语句示例：

// cover case where agent 0 req gets granted in 1 cycle
c1: cover property (req[0] ##1 gnt[0]);

// cover case where agent 0 req waits >5 cycles
c2: cover property ((req[0] && !gnt[0])[*5:$] ##1 gnt[0]);

// cover case where we see a FORCE1 arrive sometime
// while req0 is waiting
c3: cover property (opcode == FORCE1) within ((req[0] && !gnt[0])[*1:$]);

//前面声明已经全局定义过时钟和复位信号，所以在上述属性中没有出现clk 和 rst.

        使用序列而不是$rose/$fall。

       上一节中描述采样值函数时，如果要检查不是从X开始的上升值或下降值的转换，可以使用序列符号，而不是$rose或$fall。序列表达式（!mysig ##1 mysig）类似于$rose（mysig）；只是从X到1的转换时不会触发，严格检查一个时钟的mysig为0，下一个时钟为1。类似地，您可以使用（mysig ##1 !mysig）而不是$fall（mysig），以避免在从X到0的转换时触发。

2、属性语法和示例

        最常见的属性类型是使用触发蕴涵构造，sequence |-> property and sequence | => property。蕴含符的左边或者叫先行算子必须是一个sequence；右边或后续算子可以是sequence或property。

        这两个运算符之间的区别：当序列匹配时，|->在同一时钟节拍上检查property，而|=>运算符在一个节拍后检查property。当先行算子不匹配时，property会假pass。图3.10显示了一些简单属性的示例，以及它们在不同时间的真与假的轨迹。

        对于这些蕴含属性，还应该强调一点：与编写逻辑等价属性的其他方法相比，为验证提供了非常重要的优势。这是因为许多EDA工具利用了关于触发条件的信息。例如，交叠|->操作通常在逻辑上等同于简单的布尔操作，如下例所示：

a1_boolean: assert property (!cat || dog);
a1_trigger: assert property (cat |-> dog);

        使用触发版本，EDA工具可以在许多方面提供优势，以提供改进的调试功能。

• 模拟调试工具可以指示何时触发断言以及何时通过或失败的周期。
• FV工具可以生成隐式覆盖点，以检查触发条件是否可能。这也允许他们在断言被真空证明（假pass）时自动报告：因为无法满足触发条件，所以不能违反断言。

        建议如果有多种可能的方法来编写属性时，尽可能将其声明为触发蕴含。

         另一组用于构建属性的有用工具是linear temporal logic (LTL)运算符，如果想了解完整情况，将参考LRM第16.12节。

        如果要创建“liveness properties”，LTL操作符是至关重要的：指定潜在无限执行跟踪方面的属性。实践中最有用的LTL运算符可能是s_until和s_eventually。

        s_until指定一个属性必须为真，直到另一个属性（必须出现）为真，s_eventually指定某个表达式最终必须为真。这些运算符上的s_前缀代表“strong”，表示在无限追踪中，指定的条件必须在某一点发生；可以省略s_前缀以获得这些运算符的“weak”版本，这意味着不满足条件的无限跟踪不被视为违反。

        如果用户习惯于仿真，无限的轨迹听起来可能很奇怪，但它们可以通过FV工具进行分析；将在接下来的章节中进一步讨论这个问题。图3.11显示了这些LTL运算符的一些示例。

         另一类非常有用的属性是否定序列，SVA序列有一个not运算符，在序列不匹配时检查用例。

        从技术上讲，否定序列是属性对象，而不是序列对象，这意味着它不能用作蕴含运算符的先行算子。否定序列作为检查某些不安全条件是否从未发生的属性通常非常有用。下面是一些用作属性的否定序列的示例。图3.12显示了一些示例。

         与序列一样，除非包含在断言语句中，否则属性实际上没有意义。下面是一些断言语句的示例，它们可能在仲裁器模型中有用。

// assume after gnt 0, req 0 falls within 5 cycles
req0_fall_within_5: assume property
($rose(gnt[0]) |=> ##[1:5] $fell(req[0]));
// assert that any request0 is granted within 20 cycles
gnt0_within_20: assert property
($rose(req[0]) |-> ##[1:20] gnt[0])
// assert that any grant on 0 is eventually withdrawn
gnt0_fall: assert property
($rose(gnt[0]) |-> s_eventually (!gnt[0]));

3、命名序列和属性

        到目前为止，一直在断言语句中直接使用序列和属性，这是最常见的使用模式。但有时也希望将一组高级行为封装为命名对象，以便重用。

        这些类似于模块声明，但它们接受一组可选的非类型化参数；要定义命名序列，只需要关键字sequence后跟它的形式参数列表，然后是序列的表达式，最后是endsequence。

        类似地，对于属性，只需要关键字property后跟它的形式参数列表，然后是属性的表达式，最后是endproperty。通过使用属性或序列的名称并传递适当的参数，可以在断言语句或另一个属性/序列中实例化该属性/序列。

        下面是一些命名序列和属性的简单示例，以及如何使用它们：

sequence within_5_cycles(sig);
##[1:5] sig;
endsequence
property b_within_5_after_a(a,b);

a |-> within_5_cycles(b);
endproperty
// assertions a1 and a2 below are equivalent
a1: assert property (gnt[0] |-> ##[1:5] !req[0]);
a2: assert property (b_within_5_after_a(gnt[0],!req[0]));

4、断言和隐式多线程

        如果多个行为重叠，会发生什么？

        例如，假设实现了一个仲裁器，它接受每个请求作为一个周期脉冲，并期望在任何请求后10个周期获得授权。下面是描述代理0的此行为的示例断言：

delayed_gnt: assert property (req[0] |-> ##10 gnt[0]);

       由于请求和授权之间有10个周期的间隔，在该窗口内可能会有另一个请求到达。第二个请求也应该在到达后的10个周期内获得授权。所以实际上需要对这个断言进行两次重叠的评估。

        幸运的是，SVA断言提供了内置的多线程：一个断言或序列的多个实例可能在任何给定时间都在进行，每次满足其启动条件时都会触发一个新的实例。图3.13所示的波形说明了这是如何发生的。

         在图3.13中，可以看到第一个评估线程在周期1中req[0]的请求脉冲之后启动，并在周期11看到相应的授权时完成；类似地，第二个线程在周期5请求之后启动，并在周期15看到相应的授权之后结束。即使这两个断言评估是同时进行的，但它们不会相互干扰：如果授权未能在第11周期或第15周期到达，则会报告失败。

        这种隐式多线程是一把双刃剑：小心不要创建带有经常发生的触发条件的断言，否则可能会导致系统必须分析每一个周期创建的新线程，从而显著影响FV和模拟性能。

        例如，在图3.13中，以下断言将在几乎每个周期（除了周期1和5）上创建新线程：

notreq: assert property (!req[0] |-> ##10 !gnt[0]);

5、写入属性

       在实践中，如何决定何时以及如何编写断言？

        在本章的最后一节中，会提供一些关于向RTL模型添加断言的一般指南。在未来的章节中，会更具体地介绍FV中特别有用的断言示例。

        在三个主要的项目阶段，通常会定义代码中所需的断言语句：设计规格期间、RTL开发期间和验证期间。

1）在规格阶段规划属性

        在为设计生成高级规格时，应该开始考虑断言语句。描述一个具体的需求以表示设计中信号的行为时，请考虑它是否可以作为断言来编写。

        实际上，在早期阶段对RTL断言进行编码可能没有意义，但应该在规格中找到某种方法来表明现在处于断言合适的位置；当代码可用时，RTL开发人员或验证人员可以稍后插入正确的断言。

        这可以在相关段落开头加上一句“ASSERTION”， 还可以在这个阶段考虑潜在的覆盖点：这两个典型的条件都可以作为验证的一般合理性检查，以及验证可能错过的有趣的角落案例。

2）RTL开发期间的嵌入式属性

        在RTL开发过程中，RTL作者在代码中添加注释，以描述他们为什么要以某种方式实现它。

        断言可以被认为是“可执行注释”——它们有助于指明代码，但在仿真和FV期间，也提供了检查，以确保原始意图保持准确。例如，比较以下两段代码：

// Fragment 1
// We expect opcode to be in the valid range; bad
// opcode would result in bypassing these lines.
// Also, don’t forget to test each possible value.
assign forced_nodes = f_get_force_nodes(opcode);
// Fragment 2
op_ok: assert property
((opcode >= NOP)&&(opcode <= ACCESS_OFF));
generate for (i = NOP;i <= ACCESS_OFF;i++) begin: b1
test_opcode: cover property (opcode 55 i);
end
endgenerate
assign forced_nodes = f_get_force_nodes(opcode);

        可以看到，虽然这两者都传达了我们期望操作码在有效范围内的想法，并且都要求测试每个可能的操作码值，但只有片段2以可执行的方式执行这些操作。

        当RTL被传递给未来的项目以供重用时，在当今的片上系统（SOC）设计世界中几乎是肯定的，如果新用户以违反原作者假设的方式使用它，他们将在仿真或FV中看到断言失败。

        如果新用户意外禁用了原始设计中可用的一些操作码，新的验证团队将发现一些未命中的覆盖点。

        嵌入式断言编写的另一个重要方面是断言的使用，而不是假设。一般来说，在编写假设时需要小心：因为它们限制了FV使用的可能值的空间，选择不当的假设可能会适得其反或危险。特定语句需要是断言还是假设取决于运行FV的层次结构级别，大多数现代FV工具允许在工具级别动态更改特定的断言集以实现假设。

        在仿真过程中，assertions 和 assumptions是等效的。因此们建议在RTL开发期间编写嵌入式断言语句时，只编写assertions和cover points，而不是assumptions。

3）以验证为中心的属性

        另一个主要的阶段通常是为了验证而编写断言。在接下来的章节中会专注FV工作的典型属性写作风格。当专注于验证时，使用块的specification作为起点，并编写断言以SVA格式重述specification。例如，以下是仲裁器块的可能specification：

• 当opcode==FORCEn时，代理n获得授权。
• 当opcode==ACCESS_OFF时，都不会获得授权。
• 如果操作码无效，则op_error信号为1，否则为0。
• 当opcode==NOP时，仲裁工作如下：

1. 如果任何代理获得授权，编号最低的请求代理（0、1、2、3）将获得授权。
2. 当授权持有者提出请求时，请求的下一个代理将获得授权。

        如果有这样的规范，通常应该尝试编写“端到端”断言，以指定设计的输出在输入看起来如何。这些有助于发现设计中某些意外或被忽视的部分是否导致了错误行为。虽然基于内部节点的白盒断言也可以是有用的验证和调试辅助工具，但仅使用这些断言可能是危险的，因为它们关注的是设计者的低级思维过程，而不是总体设计意图。

        此外，根据设计的复杂性，通常情况下，一组简单的断言很难编写；还可能需要一些SystemVerilog建模代码来跟踪状态或计算中间值。

        不要害怕在断言中添加队列、状态机或类似的建模，这些能够正确跟踪设计行为。同时，要小心建模变得复杂到足以增加明显模拟成本的情况：只有在出现问题时，需要使用ifdefs将某些代码标记为正式代码。

        根据每个规范条件为仲裁器编写的实际断言：

• 当opcode==FORCEn时，代理n获得授权。

        期望请求/操作码和授权之间有一个周期的延迟，还需要小心地在这里包含其他代理无法获得授权的隐含要求。还应该添加适当的覆盖点，以确保验证使用此功能的情况：许多EDA工具将为直接触发条件生成自动覆盖，可能还希望添加一个明确的检查，以查看强制请求处于活动状态且获得授权的情况。因此，此需求导致以下断言语句：

parameter t_opcode fv_forces[3:0] =
{FORCE3,FORCE2,FORCE1,FORCE0};
generate for (i = 0; i <= 3;i++) begin: g1
forcei: assert property (
(opcode == fv_forces[i]) |=>
(gnt[i] == 1) && ($onehot(gnt))) else
$error(“Force op broken.”);
cover_forcei: cover property (
(opcode == fv_forces[i])
&& (gnt[i] == 1));
end
endgenerate

• 当opcode==ACCESS_OFF时，都不会获得授权。
• 如果操作码无效，则op_error信号为1，否则为0。

        这两个非常简单。但要注意错误条件：不仅需要断言无效的操作码会带来错误，而且需要断言有效的操作码不会给带来任何错误。为了更方便，创建了一个检测信号fv_validop，如下所示，还添加了一些相关的覆盖点：

accessoff: assert property (
(opcode == ACCESS_OFF) |=>
(|gnt == 0)) else
$error(“Incorrect grant: ACCESS_OFF.”);
logic fv_validop;
assign fv_validop = (opcode inside {FORCE0,FORCE1,FORCE2,
FORCE3,ACCESS_OFF,ACCESS_ON});
error0: assert property (fv_validop |=> !op_error);
error1: assert property (!fv_validop |=> op_error);
cover_nognt: cover property (|gnt == 0);
cover_err: cover property (!fv_validop ##1 !op_error);

        最后一组需求构成了仲裁器操作的核心。

• 当opcode==NOP时，仲裁工作如下|：    

1. 如果任何代理获得授权，编号最低的请求代理（0、1、2、3）将获得授权。
2. 当授权持有者提出请求时，请求的下一个代理将获得授权。

        使用一些检测函数（简单的SystemVerilog函数语句）来确定断言的循环排序中的下一个代理。这可能与设计中的某些逻辑无关，因为现在正在尝试重新检查关键实现逻辑。

// Return which bit of a one-hot grant is on
function int fv_which_bit(logic [3:0] gnt);
assert_some_owner: assert final ($onehot(gnt));
for (int i = 0; i < 4; i++) begin
if (gnt[i] == 1) begin
fv_which_bit = i;
end
end
endfunction
// Compute next grant for round-robin scheme
function logic [3:0] fv_rr_next(logic [3:0] req,
logic [3:0] gnt);
fv_rr_next = 0;
for (int i = 1; (i < 4); i++) begin
if (req[(fv_which_bit(gnt) + i)%4]) begin
fv_rr_next[(fv_which_bit(gnt) + i)%4] = 1;
break;
end
end
endfunction
// If nobody has the current grant, treat as if agent 3 had it (so agent
0,1,2 are next in priority).
rr_nobody: assert property (((opcode = NOP) &&
(|gnt == 0) && (|req == 1)) |=>
(gnt = fv_rr_next(req,4’b1000))) else
$error(“Wrong priority for first grant.”);
// If ANDing req and gnt vector gives 0, req is ended.
rr_next: assert property (((opcode == NOP) &&
(|gnt == 1) && (|req == 1) && (|(req&gnt) == 4’b0)) |=>
(gnt == fv_rr_next(req,gnt))) else
$error(“Violation of round robin grant policy.”);

        在完成要在这个块上实现的断言之前，最好看看规格书，看看是否有任何未声明的安全条件。规格中的一个常见问题：对于特定类型的设计，工程界通常会有一些隐含的概念，“不需要”对此进行说明。

        任何仲裁器都应该具有的核心安全属性：

• 从不一次将资源授予多个代理。

        这样一个明确而直接的要求确实没有任何缺点。

safety1: assert property ($onehot0(gnt)) else
$error(“Grant to multiple agents!”);

       为新模型撰写一组断言时，都要检查计划中是否有这样的缺失需求。

4）将属性与设计联系起来

        一旦编写了断言和覆盖点，就必须将它们插入到RTL模型中，最直接的方法就是将它们粘贴到top层模块的代码中。如果在设计代码时编写嵌入式断言，那么在编写代码时将它们插入到实际的RTL中是最有意义的。

        如果是出于验证目的编写断言，则可能不希望直接接触原始RTL代码。SystemVerilog提供了一个功能，使用户能够在模块内连接外部编写的代码：bind语句。

        bind语句允许将设计代码与验证代码分开，本质上强制远程模块在其内部实例化另一个模块，并像对待任何其他子模块实例一样对待它；将一组验证断言放在独立模块中，然后将其连接到模型。

        为了说明bind语句的使用，以下两个代码片段是等效的：

// Fragment 1: Directly instantiate FV module
module arbiter(...);
...
fv_arbiter fv_arbiter_inst(clk,rst,
req,gnt,opcode,op_error);
endmodule


// Fragment 2: Bind FV module
module arbiter(...);
...
endmodule
// This line may be below or in another file
bind arbiter fv_arbiter fv_arbiter_inst(clk,rst,
req,gnt,opcode,op_error);

        这样原始RTL代码可以被干净地维护，而验证代码是独立编写的，稍后连接。文章来源地址https://www.toymoban.com/news/detail-671646.html

到了这里，关于systemverilog断言简介 形式验证 第3章的文章就介绍完了。如果您还想了解更多内容，请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章，希望大家以后多多支持TOY模板网！