[经验] 基于断言的验证简介 – 第 1 部分

 

基于断言的验证简介 – 第 1 部分

 

基于断言的验证（ABV）是一种与传统方法相比可以大大减少验证过程的技术.

 

ABV主要用于 ASIC 领域，但由于FPGA 设备的复杂性不断增加，事实证明它在 FPGA 验证流程中同样至关重要。

 

然而，在我们开始庆祝芯片项目验证周期大幅缩短的可能性之前，我们需要了解断言以及如何将它们有效地集成到验证方法中。

 

为了便于技术消化，断言的介绍将分为两部分。第一部分将解释什么是断言，讨论语言并发展基本术语和思想。在第二部分中，我们将深入挖掘并介绍蕴涵的使用和“空洞真理”的概念以及断言和覆盖。

 

什么是断言？

 

断言最简单的定义是“设备行为的抽象表示，在规范、验证和实现中很有用……”

 

稍后我们会看到这个定义可以扩展为更准确的描述，但现在就用这个定义了。

 

有两种语言可用于表达断言的实际应用，即属性规范语言（PSL）和SystemVerilog断言子集（SVA） 。

 

PSL 可用于 VHDL、Verilog、 SystemVerilog和SystemC ，并且是 VHDL-2008 的子集。

 

SVA 是SystemVerilog语言的断言相关子集，基于Superlog和OpenVera捐赠。它的断言和属性功能也借鉴了 PSL。

 

两种语言都是 IEEE 标准。

 

哪种语言？

 

VHDL 设计人员可以同时使用 SVA 和 PSL，但通常选择 PSL，因为它可以直接放入 VHDL 代码中并有助于设计文档，而 SVA 则不能。此外，PSL 现在是 VHDL 标准 (2008) 的一部分，因此这意味着只需要使用一种语言。

 

Verilog 设计人员可以同时使用 PSL 和 SVA，但通常使用 SVA，因为当直接放入 Verilog 代码中时，它比 PSL 具有更多可用功能。此外， SystemVerilog和 Verilog 现在合并为一个标准 - SystemVerilog 。

 

好消息是 PSL 和 SVA 属性看起来几乎相同。

 

为什么使用断言？

 

断言已经成为 ASIC 设计中一种既定且流行的验证方法，因此 FPGA设计可以从这一领域学习。重要的是，它们受 IEEE 标准（PSL、 SystemVerilog和 VHDL）管辖。

 

面向对象编程中处理类、对象、继承等要容易得多。它们基于您作为设计师所熟悉的设计规范，因此更容易实施。

 

断言在模拟中创建了额外的安全层，因为它们是对原始规范的引用，并且在进行综合和实现迭代时非常有用。

 

断言本质上以它们的编写方式创建“实时文档”，这使得设计的管理变得更加容易。它们非常容易阅读和解释，这使得与设计团队的共享变得更容易管理。

 

在哪里放置断言？

 

所有工具都允许您将断言放置在单独的单元或文件中，并将它们“绑定”到常规 RTL 代码。验证工程师喜欢这个想法，因为它允许文件独立性，而 HDL 设计人员通常更喜欢将断言直接放入代码中以减少所需的文件量。

 

大多数模拟器允许您直接在 RTL 代码中放置断言。对于 PSL，这表示为注释。对于SystemVerilog ，断言可以直接放入代码中。

 

例如： – psl属性 p1 是... 或 // psl属性 p2 是...

 

VHDL-2008 允许将 PSL 断言直接放入代码中（无需注释）。

 

将断言放入代码中时需要小心，因为综合工具通常不支持某些断言，因此需要使用综合编译指示来管理它们。

 

发展基本术语和想法

 

术语“基于断言的验证”（ABV）通常用于描述整个验证过程，但它不仅仅涉及断言。

 

该流程由序列、属性、断言和覆盖组成。

 

ABV的基本思想是“属性”。属性是对设计的特定行为的正式描述，例如“窗户破裂触发警报”或“安全在 30 秒内响应警报”。

 

验证工具可以通过多种方式使用属性，通过“断言”属性来验证不会发生不好的事情，例如“断言损坏的窗户总是会触发警报”。

 

或者，使用“覆盖”来验证是否发生了好事，例如“在 30 秒内覆盖了对触发警报的响应”。

 

深入挖掘这些属性，如果你看一下典型的数字设计规范，它已经充满了用简单的英语表达的设计属性。作为设计人员，您可以将这些属性重写到 HDL 中，同时考虑到正确的硬件实现。

 

因此，属性、断言和覆盖代表了设计的纯粹行为（期望的或不期望的）。正如我们所说，它们可以作为非常有效的设计文档，并作为设计验证期间的参考。它们还被各种功能和形式验证工具所接受。

 

我们现在需要了解如何定义属性以及它如何使用“时间逻辑”的原理。

 

时态逻辑可以被认为是添加了时间维度的布尔逻辑。

 

如果我们使用“离散时间”，则属性表示设计的“状态序列”。请注意，所有流行的基于属性的设计 (PBD)/ABV 解决方案都对设计中对象的采样值进行操作。

 

为了及时表达这种关系，属性使用“时间”或“模态”运算符，例如下一个、最后、全局、直到（next, finally, globally, until）等。

 

接下来我们需要了解如何构建属性。

 

我们都熟悉的布尔类型表达式是属性组成的一部分，但却是最简单的部分。我们还需要了解“序列” 。

 

“序列”通常被认为是代表离散时间点上的一系列设计状态的属性的基本时间构建块。

 

典型的序列代表设计中的简单执行路径。

 

要从简单的序列创建真实的属性，您可以：

 

“融合”序列，其中一个序列在另一个序列开始的同一时刻结束。

“连接”序列，其中一个序列结束，另一个序列在下一个时间点开始

说一个序列是另一个序列的“蕴含”

“与”或“或”序列

检查一个序列是否包含在另一个序列中

检查序列是否重复给定次数（连续或不连续）

 

一旦设计属性正式化，所有工具都可以在两个指令之一中使用这些属性：

 

 

图-1

 

断言——当属性不成立时会发出警报。

 

覆盖——确认该属性已成功测试。

 

一些工具（主要是形式验证，但也有一些模拟器）允许更多指令，例如控制设计刺激或限制环境条件（假设、限制、公平等）。

 

建立实用的断言

 

现在我们已经了解了属性和序列的基本元素，让我们看看如何构建实际的断言。

 

正如我们所提到的，最基本的属性是具有严格线性时间流的“序列”。

 

模拟需要线性时间流，因此属性的时间来回跳跃是不可能的，因为这会使模拟变得不可能。

 

序列的每个节点代表您的设计的一种状态：

 

某些信号所需的值

必须满足的条件

 

为了完成序列，您必须指定如何将这些节点连接在一起。那么，让我们看看一些“序列”属性事实。

 

最简单的序列是布尔表达式，但更常见的是，您会将多个表达式粘合在一起以形成“随时间扩展”的复杂序列。

 

要使元素在同一时钟上粘在一起，请在 PSL 中使用‘fusion’ ( 或在 SVA 中使用“零时钟延迟”(##0) ‘zero clock delay’ (##0)。

 

 

 

要在元素之间引入一个周期中断，请在 PSL 中使用“串联”(;) ‘concatenation’ (;)或在 SVA 中使用“一个周期延迟”(##1) ‘one cycle delay’ (##1)。

 

 

 

您可以使用 SVA 中的一系列值 (##[ m:n ]) 指定更长的延迟。

 

PSL 使用“连续重复运算符”（<序列>[ *m 到 n]）(<sequence>[*m to n])来指定“值范围”延迟。如果没有要重复的序列，则假定“True”是重复的参数。

 

现在我们已经提到了重复，让我们更正式地看看这个。

 

如果相同的条件应保持超过一个周期，那么我们可以使用“连续重复运算符”，而不是使用串联或一个周期延迟来重复条件。

 

该运算符在 PSL 和 SVA 中看起来相同：序列 [* Number_or_Range ] Sequence [* Number_or_Range].。

 

带有数字的简单形式表示序列应该重复（保持）给定的次数： A[ *7]。

 

范围版本表示序列应在自然范围内保持任意数量的循环（要指定无限上限，请在 PSL 中使用“inf”或在 SVA 中使用“$”）： B[*1 to inf] B[*1:$]

 

 

让我们用一个例子来说明：

 

   

图3

 

在这里，我们看到了一个重复的例子，以及没有重复的等效序列，并显示了 PSL 和 SVA 的相同序列。

 

 

时钟序列/复位和属性

 

所有属性语言都使用离散时间，这意味着必须指定时钟或采样方法。

 

如果未指定时钟，则应用最快的可用工具默认值，在模拟器的情况下，这可能是周期等于模拟分辨率的时钟。

 

如果大多数属性都使用一种时钟方法，则您可以指定“默认时钟”‘default clock’。

 

要指定时钟事件，请在 PSL 中序列的末尾或 SVA 中的开头使用“@<时钟条件>”。

 

对于时钟条件，请使用本机 HDL 中首选的时钟检测器，例如VHDL 中的“ rising_edge ”函数或Verilog 中的“ negedge ”。

 

我们还需要能够处理重置，因为有时您可能正在进行属性评估，并且发生重置，这会导致断言失败或其他不需要的情况。

 

幸运的是，PSL和SVA都提供了放弃属性评估的机制，而不会产生不利影响。

 

PSL允许在属性末尾添加“ async_abort ”或“ sync_abort ”运算符和重置条件。

 

always (({(A);(B)}) async_abort C=’1′) @rising_edge(CLK);

 

在属性开头添加“disable iff （条件）”短语。

 

@(posedge CLK) disable iff (C) A ##1 B;

 

 

总结一下时钟和复位：

 

属性中没有默认重置，但您可以拥有默认时钟（采样事件）。

 

在 SVA 中将重置和时钟应用于属性的文本顺序是 PSL 中顺序的镜像。

 

   

图4

 

 

综上所述

 

我们引入了断言，并发现 PSL 和 SVA 属性相似并且类似于设计要求。

 

我们开发了断言的基本术语和思想，并讨论了序列、属性、断言和覆盖以及它们如何形成设计属性。我们还学习了如何定义属性以及它如何遵循时序逻辑原则。最后，我们开始构建一些实际的断言来理解我们所介绍和讨论的内容。

 

如果您喜欢这个介绍，您可以期待第二部分，它将介绍蕴含在断言中的使用及其在断言中的重要性以及在模拟中的使用。