1.何为断言

2.断言的作用：

3.断言的种类

3.1立即断言

3.2并发断言

4.断言层次结构

4.1 sequence 序列

4.2 property 序列

5.sequence和property的异同

6.补充知识点（assert/cover/assume）

7.写在后边

1.何为断言

断言主要用来检查仿真过程中存在的时序问题，如果存在异常情况，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。

2.断言的作用：

使用断言可以缩短研制周期；

使用断言可以使设计中存在的各种问题更容易被动态监测观察；

使用断言内嵌的覆盖率统计功能（cover）可以更加容易的获得对于功能的覆盖性；

断言的可读性较一般描述语言更容易理解；

通过全局控制实现设计中断言的开关；

断言可以加速形式验证，提高形式验证的效率；

3.断言的种类

断言分为立即断言和并行断言；

3.1立即断言

立即断言主要用来检查当前仿真时间的条件，可以理解为if...else，放在过程块中使用。

语法：

labels：assert（expression）action_block;

action_block 操作块在断言表达式的求值之后立即执行

操作块指定在断言成功或失败时采取什么操作

action_block: pass_statement; else fail_statement;

例子：

assert(expression) $display("expression evaluates to true");

else $fatal("expression evaluates to false");

断言失败默认严重程度为error，error达到一定数量仿真会退出；

立即断言构建思路：

3.2并发断言

并发断言检查跨越多个时钟周期的事件序列。

可以认为并发断言是一个连续运行的模块，为整个仿真过程检查信号，所以需要在并发断言内指定一个采样时钟。

并发断言仅在有时钟周期的情况下出现
测试表达式是基于所涉及变量的采样值在时钟边缘进行计算的
可以在过程块、module、interface和program块内定义并发断言
区别并发断言和立即断言的关键字是property

格式：

         断言名： assert property (判断条件)

例子：

        check_a_and_b:assert property (@(posedge clk) (a&&b))

                $display("a&&b is true");

        else

                 $error ("a&&b is false")；

4.断言层次结构

SVA中可以存在内建的单元，这些单元可以是以下的几种：

• Boolean expressions 布尔表达式

布尔表达式是组成断言的最小单元，断言可以由多个逻辑事件组成，这些逻辑事件可以是简单的布尔表达式.在SVA中，信号或事件可以使用常用的操作符，如：&&, ||, !, ^，& 等；

• Sequence序列

sequence是布尔表达式更高一层的单元，一个sequence中可以包含若干个布尔表达式，同时在sequence中可以使用一些新的操作符，如 ## 、重复操作符、序列操作符

• Property 属性

property是比sequence更高一层的单元，也是构成断言最常用的模块，其中最重要的性质是可以在property中使用蕴含操作符(|-> |=>)；

4.1 sequence 序列

在任何设计中，功能总是由多个逻辑事件的组合来表示，这些事件可以是简单的同一个时钟沿被求值的布尔表达式，也可以是经过几个时钟周期的求值事件，SVA用关键字sequence来表示这些事件，sequence可以让断言易读，复用性高；

sequence具有如下特性：

        • 可带参数；

        • 可以在 property 中调用；

        • 可以使用局部变量；

        • 可以定义时钟周期；

sequence的定义格式如下：

        sequence name_of_sequence(参数);

        ……

        endsequence

以下代码分别通过property，sequence+property实现对a&&b仿真时间的判断：

//1.使用property实现对a&&b时序的判断check_a_and_b:assert property(@(posedge clk) (a&&b)) $display("a&&b is true");
else     $error("a&&b is false");//2.使用sequence+property实现对a&&b时序的判断sequence seq_a_and_b;@(posedge clk) a&&b;
endsequence//在断言的property中调用sequence
check_a_and_b: assert property(seq_a_and_b) $display("a&&b is true");
else $error("a&&b is false");

sequence 序列可以带参数：

格式：

        sequence seq1(signal1,signal2);

                @(posedge clk) signal1&&signal2;

        endsequence

用法：

sequence seq1(signal1,signal2);@(posedge clk) signal1&&signal2;
endsequence//在断言的property中调用sequence
check_a_and_b: assert property(seq1(a,b)) $display("a&&b is true");
else $error("a&&b is false");

sequence 序列可以有时序

带时序关系的sequence ：在SVA中时钟延时用符号"##"来表示，如"##2"表示延时两个时钟周期；

例如：

sequence seq2;@(posedge clk) a ##2 b ;
endsequence//在断言的property中调用sequence
check_a_and_b: assert property(seq2);

sequence会在时钟上升沿到来后首先检查 a 是否为 1，当a为1时，两个时钟周期后继续检查b是否为1，当b为1时，断言pass ；

sequence 序列可以内嵌

格式

        sequence seq1;

                @(posedge clk) a&&b;

        endsequence

        sequence seq2;

                seq1;

        endsequence

4.2 property 序列

property是比sequence更高一层的单元，也是构成断言最常用的模块，其中最重要的性质是可以在

property中使用蕴含(overlapped)操作符(|-> |=>)；

property的定义格式如下：

        property name_of_property(参数列表);

                测试表达式或复杂的sequence；

        endproperty

property就是SVA中需要用来判定的部分，用来模拟过程中被验证的单元，它必须在模拟过程中被断言来发挥作用，SVA提供了关键字 assert 来检查属性，assert的基本语法是：

assertion_name: assert property(property_name)

else

        $display("SVA error");

并行断言构建思路：

5.sequence和property的异同

任何在sequence中的表达式都可以放到property中；

任何在property中的表达式也可以搬到sequence中，但是只有在property中才能使用蕴含操作符；

property中可以例化其他property和sequence，sequence中也可以调用其他sequence，但是不能例化property；

property需要用cover /assert/assume 等关键字进行实例化，而sequence直接调用即可；

除了以上的区别外，立即断言和并发断言的采样时间是否相同也是验证过程中需要注意的问题，以下的代码进行演示：

//SVA
module inline(input       clk,input        a,input        b,input [7:0]  d1,input [7:0]  d2,output[7:0]  d3,output[7:0]  d4);reg [7:0] d3=8'h0;
reg [7:0] d=48'h0;always@(posedge clk) beginif(a) begind3<=d1;endif(b) begind4<=d2;end
end
endmodulemodule top;
reg         clk;
reg         a;
reg         b;
reg [7:0]   d1;
reg [7:0]   d2;
wire [7:0]  d3;
wire [7:0]  d4;
initial begin$fsdbDumpfile("wave/top.fsdb");$fsdbDumpvars();$fsdbDumpSVA();
endinitial begin#0 clk=0;forever begin #5 clk=~clk;end
endalways begina<=$random()%2;b<=$random()%2;d1<=$random()%256;d2<=$random()%256;
end
// immesiate assertions
always@(posedge clk) begincheck_a_and_b:assert(a&&b) $display("a&&b is turn");else $error("a&&b is false");
end
// concurrent assertions
property p_mutex;@(posedge clk) not(a&&b);
endproperty
a_mutex: assert property(p_mutex)$display("a&&b is success");else $error("a&&b is fail");
initial begin#300;$finish;
endinline inline_1(clk,a,b,d1,d2,d);endmodule

波形展示：

以上代码对a&&b分别进行了immediate和concurrent assertions,波形显示两种断言结果完全相同，都在时钟上升沿前进行采样。

6.补充知识点（assert/cover/assume）

assert：

动态仿真中，如果仿真工具运行测试用例时发现断言失败，就会打印出相应的信息。

形式化验证中，assertion就是Formal验证工具（例如cadence的jasperGold）的证明目标。Formal验证工具会遍历所有的合法场景，在数学上证明这个断言永远不会失败。还是那句话，仿真只能“证伪” ，而Formal验证具有可以“证明”的能力。

cover：

动态仿真中，覆盖率是一个非常关键的数据，表明验证人员关注的场景是否真的在用例测试时被覆盖到。通常，需要确保每个测试点都至少被覆盖过一次，不然就说明我们的测试存在潜在的风险。

形式化验证中，cover也起着重要的作用。尽管理论上Formal覆盖DUT所有的场景，但是如果我们对设计过约了，可能还是会遗漏关键的场景测试。这时候，我们仍然需要使用cover来证明，我们确实对这个场景进行了有效的验证和覆盖。

assume:

动态仿真中，对于assume和assert的处理是完全相同的。EDA仿真器会在执行测试用例的时候检查assume是否失败，如果失败就会打印相应的信息。但是在概念上，assume和assert还是有些区别的：assume失败意味着验证环境或者周边设计可能出现了问题，即所测设计激励的行为不符合预期；而assert失败意味着DUT设计的行为不符合预期。

形式化验证中，assume和assert有着很明显的区别。就和字面意思一样，assume是作为设计的约束，会引导Formal工具产生的合法输入空间。如果没有assume，Formal工具会尽可能地遍历所有的空间，像空气一样到达他能够触及的空间。大多数情况，设计都会使用assume降低FPV的复杂度。

7.写在后边

关于property中的蕴含操作符部分，博主将在下一篇文章中进行总结；

博客地址：博客地址https://blog.csdn.net/weixin_45680021/article/details/131264689?spm=1001.2014.3001.5501

验证断言（立即断言并行断言）相关推荐

python unittest断言_python unittest之断言及示例
assert.png 前言 python unintest单元测试框架提供了一整套内置的断言方法. 如果断言失败,则抛出一个AssertionError,并标识该测试为失败状态如果异常,则当做错误来 ...
参数化，断言，参数化时为什么做断言，怎么做断言，如何确保断言的正确
参数化是什么参数化想必做过接口测试的各位小伙伴都不陌生,参数化是对一个接口进行多次重复类似的操作,通过将响应数据与接口API对比即可. 断言是什么手动测试时,我们通过肉眼去确认程序的实际操作后呈现 ...
java断言是什么_Java断言机制
断言概述: J2SE 1.4 在语言上提供了一个新特性,就是 assertion 功能,他是该版本在 Java 语言方面最大的革新.从理论上来说,通过 assertion 方式可以证明程序的正确性,但 ...
beanshell断言_Jmeter之BeanShell断言使用
1.Bean Shell常用内置变量 JMeter在它的BeanShell中内置了变量,用户可以通过这些变量与JMeter进行交互,其中主要的变量及其使用方法如下: log:用来记录日志文件,写入到j ...
ASV并行断言中时序的描述sequence
关键词:sequence sequence用来描述在一个或多个时钟周期内的时序关系: sequence s1;//描述时序 @(posedge clk) a ##1 b ##1 c; endseque ...
jmeter json断言_Jmeter接口测试数据库断言的实现与设计
接口测试大部分都使用接口的响应值作为接口验证的依据,但在与数据库有交互的接口中这种结果判断不足以判断接口的正确性,本文将以jmeter作为接口测试的工具来实现接口的数据库断言一. 总体思路概述 1. ...
mock测试使用断言_使用自定义断言丰富测试代码
mock测试使用断言受GeeCON会议期间@tkaczanowski演讲的启发,我决定仔细研究AssertJ库的自定义断言. 在我的"骰子"游戏中,我创建了一个"机会& ...
java断言是什么_Java断言
断言的概念断言用于证明和测试程序的假设,比如"这里的值大于 5". 断言可以在运行时从代码中完全删除,所以对代码的运行速度没有影响. 断言的使用断言有两种方法:一种是 asse ...
python断言assertequal_python中那个断言assert的优化
Python Assert 为何不尽如人意# Python中的断言用起来非常简单,你可以在assert后面跟上任意判断条件,如果断言失败则会抛出异常. Copy >>> assert ...

验证断言（立即断言并行断言）

1.何为断言

2.断言的作用：

3.断言的种类

3.1立即断言

3.2并发断言

4.断言层次结构

4.1 sequence 序列

4.2 property 序列

5.sequence和property的异同

6.补充知识点（assert/cover/assume）

7.写在后边

验证断言（立即断言并行断言）相关推荐

最新文章

热门文章