做投票链接网站,wordpress ftp服务器,phpwind与wordpress,青岛高创网站建设前言
断言主要用于验证设计的行为。断言也可用于提供功能覆盖率#xff0c;并标记用于验证的输入激励不符合假定的需求。
在验证平台中#xff0c;通常进行三个主要任务#xff1a;
产生激励功能检查功能覆盖率度量
在当今的设计越来越复杂情况下#xff0c;像波形调试…前言
断言主要用于验证设计的行为。断言也可用于提供功能覆盖率并标记用于验证的输入激励不符合假定的需求。
在验证平台中通常进行三个主要任务
产生激励功能检查功能覆盖率度量
在当今的设计越来越复杂情况下像波形调试这样的方式很容易出现人为错误因此验证平台应该有一种自动和动态地检查预期结果的方式这将使调试过程更容易也使回归测试更有效。功能检查通常针对两个特定领域
协议检查检查目标是控制信号控制信号的有效性是任何设计验证的核心数据检查检查目标是所处理数据的完整性比如网络传输的数据包是否有损坏
SystemVerilog中引入的SVA在协议检查和协议覆盖率方面可以发挥重要的作用它们更接近设计信号通过将这些断言直接连接到设计一方面便于管理另一方面仿真性能可以得到极大的提高。SVA语言本身非常简洁且提供了很好的时序控制能力。
那么什么是断言(SVA, SystemVerilog Assertion)呢我们可以找到对它的经典解释。断言是对设计属性的描述
如果在仿真中检查的属性没有按照我们期望的方式运行则断言失败如果在仿真中出现了在设计中禁止发生的行为属性则断言失败
其实简单来说就是该发生的一定要发生不应该发生的就决不能发生否则断言就失败了进而产生报错信息。
设计属性通常可以从设计的功能规范中提取并转换为断言。这些断言一方面可以用于功能仿真期间持续监控设计行为另一方面也可以通过使用Formal技术来验证设计。 SVA调度
SystemVerilog语言是基于事件(events)的执行模型。在每个time slot内把所有发生的事件按顺序排序处理。关于SV events的调度可以看下我之前写的一篇文章《详解SystemVerilog中time slot的调度》。通过遵循SV的调度算法仿真器可以避免设计和验证平台交互过程的错乱而且也让开发人员有迹可循写出稳定的代码。断言的采样、评估和执行涉及time slot里的三个regions(区域)。
Preponed该区域对断言变量进行采样。在这个区域内net和variable不会改变其状态这就允许在time slot的开始处采样到最稳定的值。Observed所有属性表达式(property expressions)都在该区域中求值。Reactive评估属性(property)的成功或失败在这个区域进行。
SystemVerilog事件调度流程图简化如图1所示。 图1 简化的SV事件调度流程图 SVA分类
SystemVerilog语言中定义了两种类型的断言Concurrent assertions(并发断言)和Immediate assertions(立即断言)。并发断言和立即断言的关键区别是property关键字。
并发断言有这几个特性
基于时钟周期基于所涉及变量在时钟边沿的采样值进行表达式求值变量的采样是在Preponed region中完成表达式的求值是在Observed region中完成可以放在procedural block, module, interface, program, general block或checker定义中可以在formal和simulation工具中使用并发断言语句可以是assert, assume, cover或restrict可以通过其可选名称来层次引用当未提供名称时工具会为其自动生成
它的定义为
concurrent_assertion_item ::[ block_identifier : ] concurrent_assertion_statement...
procedural_assertion_statement ::concurrent_assertion_statement...
concurrent_assertion_statement ::assert_property_statement| assume_property_statement| cover_property_statement| cover_sequence_statement| restrict_property_statement
assert_property_statement::assert property ( property_spec ) action_block
assume_property_statement::assume property ( property_spec ) action_block
cover_property_statement::cover property ( property_spec ) statement_or_null
cover_sequence_statement::cover sequence ( [clocking_event ] [ disable iff ( expression_or_dist ) ] sequence_expr ) statement_or_null
restrict_property_statement::restrict property ( property_spec ) ; 图2 并发断言定义 立即断言有这几个特性
基于simulation events语义表达式的求值与procedural block中的任何其它Verilog表达式一样本质上是立即求值的必须放在procedural block定义中仅用于simulation工具中使用立即断言语句可以是assert, assume或cover
它的定义为
procedural_assertion_statement ::...| immediate_assertion_statement...
immediate_assertion_statement ::simple_immediate_assertion_statement| deferred_immediate_assertion_statement
simple_immediate_assertion_statement ::simple_immediate_assert_statement| simple_immediate_assume_statement| simple_immediate_cover_statement
simple_immediate_assert_statement ::assert ( expression ) action_block
simple_immediate_assume_statement ::assume ( expression ) action_block
simple_immediate_cover_statement ::cover ( expression ) statement_or_null
deferred_immediate_assertion_item :: [ block_identifier : ] deferred_immediate_assertion_statement
deferred_immediate_assertion_statement ::deferred_immediate_assert_statement| deferred_immediate_assume_statement| deferred_immediate_cover_statement
deferred_immediate_assert_statement ::assert #0 ( expression ) action_block| assert final ( expression ) action_block
deferred_immediate_assume_statement ::assume #0 ( expression ) action_block| assume final ( expression ) action_block
deferred_immediate_cover_statement ::cover #0 ( expression ) statement_or_null| cover final ( expression ) statement_or_null
action_block ::statement _or_null| [ statement ] else statement_or_null 图3 立即断言定义 断言的声明关键字有以下类型(属性大家可以把它理解成一种设计行为)
assert: 这个关键字是大家最常见的它指定属性为要检查的设计行为并验证该属性是否成立assume: 指定属性作为环境的假设。Formal工具使用该信息生成输入激励仿真器检查属性是否成立cover: 收集属性是否被覆盖到restrict: 指定属性作为formal验证计算的约束仿真器不需要检查该属性可以看出这个关键字是不用于立即断言的 构建SVA模块
立即断言的构建比较简单直接写上assert/assume/cover statement就好了。这一小节主要是讲并发断言的构建它有很多种构建方式这里列下比较常用的方式。
在任何设计模型中功能都由多个逻辑事件的组合表示。这些事件可以是在同一时钟边沿计算的简单布尔表达式也可以是涉及多个时钟周期的一段时间内计算的事件。SVA提供了一个关键字来表达这些事件称为“sequence”。sequence的基本语法如下所示
sequence name_of_sequence; test_ expression ;
endsequence
图4 sequence的基本语法 许多sequences可以按逻辑或顺序组合以创建更复杂的sequences。SVA提供了一个关键字来表示这些复杂的顺序行为称为“property”。property的基本语法如下所示
property name_of_property; test expression ; or complex sequence expressions ;
endproperty
图5 property的基本语法 property是在仿真期间生效并进行验证的SVA提供了一个“assert”的关键字来检查property。assert的基本语法如下所示
assertion_name : assert property ( property_name ) ;
图6 assert的基本语法 因此创建并发SVA断言所涉及的通用步骤如下图7所示。 图7 创建并发SVA断言通用步骤 例子
5.1 立即断言例子
下面代码为立即断言的一个简单例子
always_comb beginia_blk: assert(a b);
end 立即断言ia_blk是作为procedural块的一部分写入的它遵循信号“a”和“b”的相同事件调度也就是如果信号“a”和“b”发生变化那么always_comb块就执行。ia_blk的仿真结果如图8所示。断言成功用向上蓝色箭头表示断言失败用向下红色箭头表示。 图8 立即断言ia_blk仿真结果 5.2 并发断言例子
下面代码为并发断言的一个简单例子
sequence s_ab;a b;
endsequenceproperty p_ab;(posedge clk) s_ab;
endpropertyca_blk: assert property (p_ab); 并发断言ca_blk的结果如图9所示。同样的所有的成功用向上蓝色箭头表示所有的失败用向下红色箭头表示。这个例子中的关键概念是无论信号“a”和信号“b”是否改变该属性都在时钟clk的每个上升沿上求值检查。 图9 立即断言ca_blk仿真结果 将立即断言和并发断言对ab的仿真检查结果放在一起结果如图10所示。 图10 立即断言和并发断言对ab的仿查结果 从这个结果可以看出立即断言procedural block中的任何其它Verilog表达式一样都是当个cycle立即求值的。而并发断言有点像使用default input #1step的clocking block中的信号采样求值。 总结
本文主要是从大框架上梳理SVA的知识点从为什么需要SVA有什么好处SVA分类SVA调度和检查机制、以及举了两个简单直观的例子帮忙读者们快速get到SVA的全貌。有了这个宏观了解对于比较细节(微观)的语法大家可以翻翻工具书看看或者用到的时候再查找下。 往期精彩内容
芯片验证分享系列总结及PPT分享
