何为断言？断言的作用有哪些？断言的种类 断言层次结构
01 何为断言
断言主要用来检查仿真过程中存在的时序问题，如果存在异常情况，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。
02 断言的作用
· 使用断言可以缩短研制周期；
· 使用断言可以使设计中存在的各种问题更容易被动态监测观察；
· 使用断言内嵌的覆盖率统计功能（cover）可以更加容易的获得对于功能的覆盖性；
· 断言的可读性较一般描述语言更容易理解；
· 通过全局控制实现设计中断言的开关；
· 断言可以加速形式验证，提高形式验证的效率；
03 断言的种类
断言分为立即断言和并行断言
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)；
04 断言层次结构
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中调用sequencecheck_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中调用sequencecheck_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中调用sequencecheck_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);
并行断言构建思路：
05 sequence和property的异同
· 任何在sequence中的表达式都可以放到property中；
· 任何在property中的表达式也可以搬到sequence中，但是只有在property中才能使用蕴含操作符；
· property中可以例化其他property和sequence，sequence中也可以调用其他sequence，但是不能例化property；
· property需要用cover /assert/assume 等关键字进行实例化，而sequence直接调用即可。
除了以上的区别外，立即断言和并发断言的采样时间是否相同也是验证过程中需要注意的问题，以下的代码进行演示：
//svamodule 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;endendendmodulemodule 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; endendalways begina<=$random()%2;b<=$random()%2;d1<=$random()%256;d2<=$random()%256;end// immesiate assertionsalways@(posedge clk) begincheck_a_and_b:assert(a&&b) $display(a&&b is turn);else $error(a&&b is false);end// concurrent assertionsproperty p_mutex;@(posedge clk) not(a&&b);endpropertya_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,波形显示两种断言结果完全相同，都在时钟上升沿前进行采样。
06 补充知识点
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的复杂度。
用简单明了的方法教你使用定时器中断
教你做一个电子打火机
北京推出自动驾驶测试管理方案 确保测试的规范化
苹果 Apple Watch 异常天气条件下会给出不正确的海拔读数，只能重置
顺启顺停电路实际接线及原理
何为断言？断言的作用有哪些？断言的种类 断言层次结构
电视面板报价开始全面止跌 面板厂亏损扩大
羚羊平台承办长三角工业互联网峰会，洞见行业未来！
PI将参加深圳 PCIM Asia 2021并展示电源转换等方案
光电传感器的常见故障及解决方法解析
新唐科技NCT5532D芯片简介
电动汽车销量持续下滑，宁德时代和比亚迪打击不小
未来的智慧城市会发展成什么样
包装用智能标签的发展情况怎样了
自动驾驶又出“商业间谍”，新能源汽车核心专利是关键
华硕推出 TUF Gaming Radeon RX 6900 XT 显卡，2.9 槽设计
智能型可燃气体报警器有什么优势
总投资10亿,泰科天润六英寸SiC项目落户江西九江
用可编程模拟器件实现直流伺服电机的速度控制
苹果挑战亚马逊 智能音箱大战为何外热内冷？
断言主要用来检查仿真过程中存在的时序问题，如果存在异常情况，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。
02 断言的作用
· 使用断言可以缩短研制周期；
· 使用断言可以使设计中存在的各种问题更容易被动态监测观察；
· 使用断言内嵌的覆盖率统计功能（cover）可以更加容易的获得对于功能的覆盖性；
· 断言的可读性较一般描述语言更容易理解；
· 通过全局控制实现设计中断言的开关；
· 断言可以加速形式验证，提高形式验证的效率；
03 断言的种类
断言分为立即断言和并行断言
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)；
04 断言层次结构
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中调用sequencecheck_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中调用sequencecheck_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中调用sequencecheck_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);
并行断言构建思路：
05 sequence和property的异同
· 任何在sequence中的表达式都可以放到property中；
· 任何在property中的表达式也可以搬到sequence中，但是只有在property中才能使用蕴含操作符；
· property中可以例化其他property和sequence，sequence中也可以调用其他sequence，但是不能例化property；
· property需要用cover /assert/assume 等关键字进行实例化，而sequence直接调用即可。
除了以上的区别外，立即断言和并发断言的采样时间是否相同也是验证过程中需要注意的问题，以下的代码进行演示：
//svamodule 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;endendendmodulemodule 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; endendalways begina<=$random()%2;b<=$random()%2;d1<=$random()%256;d2<=$random()%256;end// immesiate assertionsalways@(posedge clk) begincheck_a_and_b:assert(a&&b) $display(a&&b is turn);else $error(a&&b is false);end// concurrent assertionsproperty p_mutex;@(posedge clk) not(a&&b);endpropertya_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,波形显示两种断言结果完全相同，都在时钟上升沿前进行采样。
06 补充知识点
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的复杂度。
用简单明了的方法教你使用定时器中断
教你做一个电子打火机
北京推出自动驾驶测试管理方案 确保测试的规范化
苹果 Apple Watch 异常天气条件下会给出不正确的海拔读数，只能重置
顺启顺停电路实际接线及原理
何为断言？断言的作用有哪些？断言的种类 断言层次结构
电视面板报价开始全面止跌 面板厂亏损扩大
羚羊平台承办长三角工业互联网峰会，洞见行业未来！
PI将参加深圳 PCIM Asia 2021并展示电源转换等方案
光电传感器的常见故障及解决方法解析
新唐科技NCT5532D芯片简介
电动汽车销量持续下滑，宁德时代和比亚迪打击不小
未来的智慧城市会发展成什么样
包装用智能标签的发展情况怎样了
自动驾驶又出“商业间谍”，新能源汽车核心专利是关键
华硕推出 TUF Gaming Radeon RX 6900 XT 显卡，2.9 槽设计
智能型可燃气体报警器有什么优势
总投资10亿,泰科天润六英寸SiC项目落户江西九江
用可编程模拟器件实现直流伺服电机的速度控制
苹果挑战亚马逊 智能音箱大战为何外热内冷？