毛主席说过:人不犯我我不犯人,人若犯我我必犯人。
目录
1.2 为什么用System Verilog 断言(SVA)
断言是设计的属性描述。
????????●如果一个在模拟中被检查的属性(property)不像我们期望的那样表现,那么这个断言失败。
????????● 如果一个被禁止在设计中出现的属性在模拟过程中发生,那么这个断言失败。
?一系列的属性可以从设计的功能描述中推知,并且被转换成断言。这些断言能在功能的模拟中不断地被监视。使用形式验证技术,相同的断言能被重用来验证设计。断言,又被称为监视器或者检验器,已经被用作一种调试技术的方式,在设计验证流程中使用了很长时间。传统上,它们由过程语言,比如 Verilog,来实现。它们也能用 PLI 和 C/C++的程序来实现。下面的代码显示了相互断言条件检查的 Verilog 实现,其中信号 a 和信号 b不能同时为高电平。如果这种情况发生,则显示这是一个错误信息。
?这种监视器仅作为模拟的一部分而存在,因此只有当需要时才被纳入设计环境中。这可以通过允许 Verilog 代码条件编译的指令“ `ifdef”来实现。
虽然 Verilog 可以很容易地用来实现一些检查,它仍有一些不足之处:
????????(1) Verilog 是一种过程语言,因此并不能很好地控制时序。
????????(2) Verilog 是一种冗长的语言,随着断言的数量增加,维护代码将变得很困难。
????????(3) 语言的过程性这一本质使得测试同一时间段内发生的并行事件相当困难。在一些情况下,一个 Verilog 的检验器甚至可能无法捕捉到所有被触发的事件。
????????(4) Verilog 语言没有提供内嵌的机制来提供功能覆盖的数据。用户必须自己实现这部分代码。
SVA 是一种描述性语言,可以完美地描述时序相关的状况。语言的描述性本质提供了对时间卓越的控制。语言本身非常精确且易于维护。 SVA 也提供了若干个内嵌函数来测试特定的设计情
况,并且提供了一些构造来自动收集功能覆盖数据。
例子 1.1 显示了分别用 Verilog 和 SVA 实现的检验器。
这个检验器验证当信号 a 在当前时钟周期为高电平时,下面 1~3 个时钟周期内,信号 b 应该变为高电平。
?
?通过这幅图也可以清晰的看到前两次的判断都是成功的,最后一次是失败的。
?SystemVerilog 语言被定义成一种基于事件的执行模式。在每个时隙(time slot),许多事件按照安排的顺序发生。这个事件的列表依照标准定义的算法执行。依照这个算法,模拟器可以防止任
何在设计和测试平台互动中的不一致。断言的评估和执行包括以下三个阶段:
预备(Preponed) 在这个阶段,采样断言变量,而且信号(net)或变量(variable)的状态不能改变。这样确保在时隙开始的时候采样到最稳定的值。
观察(Observed) 在这个阶段,对所有的属性表达式求值。
响应(Reactive) 在这个阶段,调度评估属性成功或失败的代码。
图 1-2 显示了一个简化了的 SystemVerilog 事件进程安排流程表 。
?SystemVerilog 语言中定义了两种断言:并发断言和即时断言。
基于时钟周期。
● 在时钟边缘根据调用的变量的采样值计算测试表达式。
● 变量的采样在预备阶段完成,而表达式的计算在调度器的观察阶段完成。
● 可以被放到过程块(procedural block)、模块(module)、接口(interface),或者一个程序(program)的定义中。
● 可以在静态(形式的)验证和动态验证(模拟)工具中使用。一个并发断言的例子如下:
?
?a的波形晚时钟一个Δclk,b的波形与时钟同步。箭头朝上显示成功,所有的失败显示成向下的箭头。这个例子的核心内容是属性在每一个时钟的上升沿都被检验,不论信号 a 和信号 b 是否有值的变化。
●基于模拟事件的语义。
● 测试表达式的求值就像在过程块中的其他 Verilog 的表达式一样。它们本质不是时序相关的,而且立即被求值。
● 必须放在过程块的定义中。
● 只能用于动态模拟
一个即时断言的例子如下:
?
即时断言 a_ia 被写成一个过程块的一部分,它遵循和信号 a、b 相同的事件调度。当信号 a 或者信号 b 发生变化时, always 块被执行。区别即时断言和并发断言的关键词是“ property”。
在任何设计模型中,功能总是由多个逻辑事件的组合来表示的。这些事件可以是简单的同一个时钟边缘被求值的布尔表达式,或者是经过几个时钟周期的求值的事件。 SVA 用关键词“ sequence”
来表示这些事件。序列(sequence)的基本语法是:
许多序列可以逻辑或者有序地组合起来生成更复杂的序列。SVA 提供了一个关键词“ property”来表示这些复杂的有序行为。属性(property)的基本语法是:
属性是在模拟过程中被验证的单元。它必须在模拟过程中被断言来发挥作用。 SVA 提供了关键词“ assert”来检查属性。断言(assert)的基本语法是:
建立 SVA 检验器的步骤如图 1-5 所示:
?
序列 s1 检查信号“ a”在每个时钟上升沿都为高电平。如果信号“ a”在任何一个时钟上升沿不为高电平,断言将失败。注意,这相当于“ a == 1’b1”。
?
?
a信号的波形相较clk时钟往后延迟了一个Δclk
序列 s1 使用的是信号的逻辑值。 SVA 也内嵌了边缘表达式,以便用户监视信号值从一个时钟周期到另一时钟周期的跳变。这使得用户能检查边沿敏感的信号。三种这样有用的内嵌函数如下:
$rose(boolean expression or signal_name)
● 当信号/表达式的最低位变成 1 时返回真。
$fell(boolean expression or signal_name)
● 当信号/表达式的最低位变成 0 时返回真。
$stable(boolean expression or signal_name)
● 当表达式不发生变化时返回真。
序列 s2 检查信号“ a”在每一个时钟上升沿都跳变成 1。如果跳变没有发生,断言失败。
?
?信号a相较于CLK延迟一个ΔCLK
?序列 s3 检查每一个时钟上升沿,信号“ a”或信号“ b”是高电平。如果两个信号都是低电平,断言失败。
?通过在序列定义中定义形参,相同的序列能被重用到设计中具有相似行为的信号上。例如,我们可以定义下面这个序列
通用的序列 s3_lib 能重用在任何两个信号上。例如,我们有两个信号“ req1”和“ req2”,它们中至少一个信号应该在时钟周期的上升沿为 1,我们可以使用下列的序列。
一些在设计中常见的通常的属性可以被开发成一个库以便于重用。比如, one-hot 状态机检查,等效性检查等都适合放在这样的检验器库中。
简单的布尔表达式在每个时钟边缘都会被检查。换句话说,它们只是简单的组合逻辑检查。很多时候,我们关心的是检查需要几个时钟周期才能完成的事件。也就是所谓的“时序检查”。
在 SVA 中,时钟周期延迟用“ ##”来表示。例如, ##3 表示 3 个时钟周期。
序列 s4 检查信号“ a”在一个给定的时钟上升沿为高电平,如果信号“ a”不是高电平,序列失败。如果信号“ a”在任何一个给定的时钟上升沿为高电平,信号“ b”应该在两个时钟周期后为高电平。如果信号“ b”在两个时钟周期后不为 1,断言失败。
注意,序列以信号“ a”在时钟上升沿为高电平开始。
?
?与前面小节中的例子不同的是,序列 s4 的开始时间和结束时间不同。如果信号“ a”在任何时钟周期不为高电平,序列在同一个时钟周期开始并失败。如果信号“ a”是高电平,序列开始。在两个时钟周期后,如果信号“ b”是高电平,序列成功(第 5 和第14 时钟周期)。另一方面,如果在两个时钟周期后,信号“ b”不是高电平,序列失败。应注意的是,在图中,成功的序列总是标注在序列开始的位置。
?
?信号A相较于Clk延迟ΔCLK
一个序列或者属性在模拟过程中本身并不能起什么作用。它们必须像下面的例子那样被断言才能发挥作用。
注意,序列 s5 中指定了时钟。这是一种把检查和时钟关联起来的方法,但是还有其他的方法。在序列、属性,甚至一个断言的语句中都可以定义时钟。下面的代码显示了在属性 p5a 的定义中指定时钟。
?通常情况下,在属性(property)的定义中指定时钟,并保持序列(sequence)独立于时钟是一种好的编码风格。这可以提高基本序列定义的可重用性。
断言一个序列并不一定需要定义一个独立的属性。因为断言语句调用属性,在断言的语句中可以直接调用被检查的表达式,如下面的断言 a5b 所示。
?当我们在断言的陈述中要调用已经定义了时钟的序列,就不能再次在断言语句中定义时钟。下面的断言 a5c 就显示了这种错误的编程风格。
在之前的所有例子中,属性检查的都是正确的条件。属性也可以被禁止发生。换句话说,我们期望属性永远为假。当属性为真时,断言失败。
序列 s6 检查当信号“ a”在给定的时钟上升沿为高电平,那么两个时钟周期以后,信号“ b”不允许是高电平。关键词“ not”用来表示属性应该永远不为真。
?
?
SystemVerilog 语言被定义成每当一个断言检查失败,模拟器在默认情况下都会打印出一条错误信息。模拟器不需要对成功的断言打印任何东西。读者同样也可以使用断言陈述中的“执行块”
(action block)来打印自定义的成功或失败信息。执行块的基本语法如下所示。
下面显示的检验器 a7 在执行块中使用了简单的显示语句来打印成功和失败信息。
?属性 p7 有下列特别之处:
(1) 属性在每一个时钟上升沿寻找序列的有效开始。在这种情况下,它在每个时钟上升沿检查信号“ a”是否为高。
(2) 如果信号“ a”在给定的任何时钟上升沿不为高,检验器将产生一个错误信息。这并不是一个有效的错误信息,因为我们并不关心只检查信号“ a”的电平。这个错误只表明我们在这个时钟周期没有得到检验器的有效起始点。 虽然这些错误是良性的,它们会在一段时间内产生大量的错误信息,因为检查在每个时钟周期都被执行。为了避免这些错误, 某种约束技术需要被定义来在检查的起始点不有效时忽略这次检查。
SVA 提供了一项技术来实现这个目的。这项技术叫作“蕴含”(Implication)。
蕴含等效于一个 if-then 结构。蕴含的左边叫作“先行算子”(antecedent),右边叫作“后续算子” (consequent)。先行算子是约束条件。当先行算子成功时,后续算子才会被计算。如果先行算
子不成功,那么整个属性就默认地被认为成功。这叫作“空成功”(vacuous success)。蕴含结构只能被用在属性定义中,不能在序列中使用。
蕴含可以分为两类:交叠蕴含(Overlapped implication)和非交叠蕴含(Non-overlapped implication)。
?
交叠蕴含用符号“ |->”表示。如果先行算子匹配,在同一个时钟周期计算后续算子表达式。下面用一个简单的例子解释。属性 p8 检查信号“ a”在给定的时钟上升沿是否为高电平,如果 a为高,信号“ b”在相同的时钟边沿也必须为高。
图 1-11 显示了断言 a8 在模拟中的响应。 表 1-5 总结了信号“ a”和信号“ b”的采样值和断言的状态。表中一共显示了三种结果。当信号“ a”检测为有效的高电平,而且信号“ b”在同一个时钟沿也检测为高,这是一个真正的成功。若信号“ a”不为高,断言默认地自动成功,则称为空成功。相应的,失败指的是信号“ a”检测为高且在同一个时钟沿信号“ b”未能检测为有效的高电平。
?
非交叠蕴含用符号“ |=>”表示。如果先行算子匹配,那么在下一个时钟周期计算后续算子表达式。后续算子表达式的计算总是有一个时钟周期的延迟。下面以属性 p9 举个简单的例子。该属
性检查信号“ a”在给定的时钟上升沿是否为高,如果为高,信号“ b”必须在下一个时钟边沿为高。
?
?
属性 p10 检查如果信号“ a” 在给定时钟上升沿为高,在两个时钟周期后信号“ b”应该为高。类似的检查在前面已经用不使用蕴含的方式介绍过了。使用蕴含使得所有误报的错误都被消除。只有属性有效开始(信号“ a”为高)时,才进行后续算子的检查(信号“ a” )。图 1-13 显示了属性 p10 的一个模拟的例子。
?
属性 p10 在先行算子的位置使用的是信号。先行算子同样可以使用序列的定义。在这种情况下,仅当先行算子中的序列成功时,才计算后续算子中的序列或者布尔表达式。在任何给定的时钟周期,序列 s11a 检查如果信号“ a”和信号“ b”都为高,一个时钟周期之后信号“ c”应该为高。序列 s11b 检查当前时钟上升沿的两个时钟周期后,信号“ d”应为低。最终的属性检查如果序列 s11a 成功,那么序列 s11b 被检查。如果没有监测到有效的序列s11a,那么序列 s11b 将不被检查,属性检查得到一次空成功。
?
到目前为止,带延迟的例子使用的都是固定的正延迟。在下面几个例子中,我们将讨论几种不同的描述延迟的方法。属性 p12 检查布尔表达式“ a && b”在任何给定的时钟上升沿为真。如果表达式为真,那么在接下去的 1~3 周期内,信号“ c”应该至少在一个时钟周期为高。 SVA 允许使用时序窗口来匹配后续算子。时序窗口表达式左手边的值必须小于右手边的值。左手边的值可以是 0。如果它是 0,表示后续算子必须在先行算子成功的那个时钟边沿开始计算。
图 1-15 显示了属性 p12 在模拟中的响应。每声明一个时序窗口,就会在每个时钟沿上触发多个线程来检查所有可能的成功。
p12 实际上以下面三个线程展开。
(a && b) |-> ##1 c 或
(a && b) |-> ##2 c 或
(a && b) |-> ##3 c
属性有三个机会成功。所有三个线程具有相同的起始点,但是一旦第一个成功的线程将使整个属性成功。应当注意,在任何时钟上升沿只能有一个有效的开始,但是可以有多个有效的结束。这是因为每个有效的起始可以有三个机会成功。
属性 p13 与属性 p12 相似。两者最大的区别是 p13 的后续算子在先行算子成功的同一个时钟沿开始计算。
?
?图 1-16 显示了 p13 在模拟中的响应。与属性 p12 最大的区别在于一个成功的开始发生在时钟周期 12。这个成功是因为检查发生了重叠。信号“ c”的值在先行算子成功的同一个时钟沿被检测为高。
在时序窗口的窗口上限可以用符号“ $”定义,这表明时序没有上限。这叫作“可能性” (eventuality)运算符。检验器不停地检查表达式是否成功直到模拟结束。因为会对模拟的性能产生巨大的负面影响,所以这不是编写 SVA 的一个高效的方式。最好总是使用有限的时序窗口上限。
属性 p14 在任何给定的时钟上升沿检查信号“ a”是否为高。如果为高,那么信号“ b”从下一个时钟周期往后最终将为高,而信号“ c”在信号“ b”为高的时钟周期开始往后最终将为高。
?
笔者为什么要写这篇文章,原因是之前在一家公司里面,管我的验证小领导,怎么看我不顺眼,觉得我什么也不会,就是想逼我离职。总是拿SV断言说事,语气中充斥着各种轻蔑与鄙视,斜眼看人的不屑的表情让我很难受,真的很难受。
对于帮助过我的人,永远心存感恩。只是痛苦的记忆是我不能释怀。这篇文章整体而言比较简单明了,如果你没有太多的时间的话,没有关系,看一下,基本上就都会了!
持续更新......