【IC每日一题：SVA简介】

IC每日一题：SVA简介

1 断言概念
- 1.1 断言优势；
- 1.2 断言类型
- - 1.2.1 立即断言
  - 1.2.2 并行断言
  - 1.2.3 并发断言Demo
2 SVA语法
- 2.1 蕴含操作符：|-> 和 ->
- - 2.1.1 蕴含操作符 |=>
  - 2.1.2 蕴含操作符|->
- 2.2 延时操作符
- - 2.2.1 ##n 操作符
- 2.3 重复操作符
- - 2.3.1 [*n]操作符
  - 2.3.2 [->n]操作符
  - 2.3.3 [=n]操作符
  - 2.3.4 [*]操作符
  - 2.3.5 [=0]操作符
  - 2.3.6 [->0]操作符
- 2.4 匹配操作符
- - 2.4.1 intersect操作符
  - 2.4.2 within操作符
  - 2.4.3 throught操作符
  - 2.4.4 before操作符
  - 2.4.5 first_match操作符
  - 2.4.6 s_next 操作符
- 2.5 内键函数
- - 2.5.1 $rose函数
  - 2.5.2 $fell
  - 2.5.3 $stable
  - 2.5.4 $past
  - 2.5.5 others
3 FIFO空满断言

【博客首发于微信公众号《漫谈芯片与编程》，欢迎专注一下，多谢大家】

断言是对设计的属性的描述，用以检查设计是否按照预期执行。断言常用来验证总线时序或其他特定的时序逻辑，找出设计中的违例等。
断言主要用于验证设计的行为。断言是在仿真期间嵌入设计中或绑定到设计单元的检查。当特定条件或事件序列失败时，会生成警告或错误。设计人员可以在设计中嵌入断言立即报出error；验证人员编写断言用于验证及时设计错误和创建断言覆盖率；

1 断言概念

1.1 断言优势；

SVA 使用简洁的语法来描述复杂的时序和逻辑关系，使得断言易于阅读和维护；
相比于用verilog进行检查，SVA的优势在于：
1.SVA非常适合描述检查协议时序相关状况；
2.内部提供许多内嵌函数，方便直接调用；
3.可以创建断言覆盖率进行手机，定量检查；

1.2 断言类型

1.2.1 立即断言

立即断言：非时序，执行如过程语句，立即断言语句是在过程代码执行时对表达式进行的测试。如果表达式的值为X、Z或0，则解释为假，并且断言失败。否则，表达式解释为真，断言通过。可以在initial/always过程块中或者task/function中使用。立即断言可以结合 $f a t a l,$ error, $w a r nnin g,$ info;

[name: ] assert(expression) [pass_statement][else fail_statement]

注意事项：

如果表达式计算结果为真，则执行 pass 语句。
与 else 关联的语句称为 fail 语句，如果表达式计算结果为假，则执行该语句。
pass 和 fail 语句都是可选的。
由于断言是一种必须为真的声明，断言失败将具有相关的严重性。默认情况下，断言失败的严重性为错误。
可以通过在 fail 语句中包含以下严重性系统任务之一来指定其他严重性级别：
$fatal - 生成运行时致命断言错误，终止仿真并返回错误代码。
$error - 是一个简单的 SystemVerilog 构造，发出错误严重性消息。
$warning - 是一个运行时警告，可以以工具特定的方式抑制。
$info - 表示断言失败没有特定的严重性。
如果断言失败且未指定 else 子句，则工具默认调用 $error。

非常类似if-else表达四

1.2.2 并行断言

并行断言：时序性的、需要使用关键词proper，与设计模块并行执行，并行断言只会在时钟边沿激活，变量的值是采样得到的值。

检查分布在多个时钟周期上的事件序列的断言称为并发断言。
它们与其他 always 块并行执行，因此称为并发断言。
与立即断言不同，同时断言仅在时钟节拍时进行评估。因此，它是一种基于时钟的评估模型，并且在并发断言中使用的表达式始终与时钟定义相关联。
用于区分立即断言和并发断言的关键字是 “property”。

1.创建并发断言步骤

序列：在任何设计模型中，功能由多个逻辑事件的组合表示；这些事件可以是在相同时钟边沿上计算的简单布尔表达式，也可以是在一段时间内涉及多个时钟周期的事件。关键字是"sequence".

sequence name_of_sequence;  <test expression> 
endsequence

属性：可以逻辑地或按顺序组合多个序列以创建更复杂的序列；关键字“property”.

property name_of_property;<test expression> or  <complex sequence expressions>
endproperty

断言：属性是在仿真期间验证的属性。必须断言该属性以在仿真期间生效；关键字–assert；

assertion_ name: assert property( property_name );

** 对于较为简单的时序逻辑关系，可以不单独定义sequence，将sequence的内容直接写在property中；而对于时序关系较复杂的，或者为了提高复用性，可以将一些时序逻辑定义为单独的sequence，然后在property中调用。**

1.2.3 并发断言Demo

//----sequence----property---assertsequence seq;@(posedge clk) (A==1 && B==1);endsequenceproperty ppt;seq;endpropertyassert property (ppt) $display(" %0t, A=1 and B=1, assertion success",$time);else $display("%0t, A=%0b and B=%0b,assertion failure", $time,A,B);//---property--assert// 属性property req_ack_prop;@(posedge clk) req |-> ack;  // 当 req 为高时，下一个时钟周期 ack 也必须为高endpropertyproperty req_nack_prop;@(posedge clk) req |-> !ack;  // 当 req 为高时，下一个时钟周期 ack 不能为高endproperty// 断言assert property (req_ack_prop)else $error("Assertion failed: req_ack_prop");assert property (req_nack_prop)else $error("Assertion failed: req_nack_prop");//=====覆盖======//
// 覆盖cover property (req_ack_prop);

SVA_105">2 SVA语法

2.1 蕴含操作符：|-> 和 ->

蕴含操作符只能在property中使用；
如果我们希望仅在 “a” 高电平之后检查序列，可以通过使用蕴含运算符来实现。蕴含等价于一个 if-then 结构。
蕴含的左侧称为“前提”，右侧称为“结果”。
它只能用于属性定义，不能用于序列。

a |-> b：如果a成立，那么在当前时刻b必须成立；
a |=> b：如果a成立，那么在下一时刻b必须成立；

2.1.1 蕴含操作符 |=>

语法: A |=> B
含义: 如果 A 成立，则在下一个时钟周期 B 必须成立。
特点: |=> 是一个隐含的蕴含操作符，通常用于描述时序关系。它默认在时钟边沿处进行采样。

property req_ack;@(posedge clk) req |=> ack;  // 如果 req 在时钟上升沿成立，则在下一个时钟上升沿 ack 必须成立
endpropertyassert property (req_ack)else $error("Assertion failed: req_ack");//====带复位
property req_ack_with_reset;@(posedge clk) disable iff (!rst_n) req |=> ack;  // 如果 req 在时钟上升沿成立，则在下一个时钟上升沿 ack 必须成立，除非复位信号 rst_n 为低
endpropertyassert property (req_ack_with_reset)else $error("Assertion failed: req_ack_with_reset");//====带复位和组合逻辑
property complex_property;@(posedge clk) disable iff (!rst_n)(req && !ack) |=> (ack ##1 data_valid);  // 如果 req 成立且 ack 未成立，则在下一个时钟周期 ack 必须成立，并且在再下一个时钟周期 data_valid 必须成立
endpropertyassert property (complex_property)else $error("Assertion failed: complex_property");

2.1.2 蕴含操作符|->

如果前提匹配，则结果表达式将在同一个时钟周期中计算。

    property p;@(posedge clk) a |-> b;endproperty  a: assert property(p);

2.2 延时操作符

2.2.1 ##n 操作符

语法: A ##n B
含义: A 发生后，经过 n 个时钟周期，B 必须发生。
特点: 用于描述信号之间的固定时钟周期延迟。

property req_ack_delay;@(posedge clk) req ##1 ack;  // 如果 req 在时钟上升沿成立，则在下一个时钟上升沿 ack 必须成立
endpropertyassert property (req_ack_delay)else $error("Assertion failed: req_ack_delay");property p;@(posedge clk) a |-> ##[1:4] b;//在当前时钟沿检查到a=1后，检测接下来的1~4个时钟周期内b=1
endproperty
a: assert property(p);property p;@(posedge clk) a |-> ##[0:4] b;//在当前时钟沿检查到a=1后，检测接下来的0~4个时钟周期内b=1，也就是在当前时钟沿b也必须为1
endproperty
a: assert property(p);property p;@(posedge clk) a |-> ##[1:$] b;//在当前时钟沿检查到a=1后，检测下一个时钟周期到仿真时间结束b=1
endproperty
a: assert property(p);

2.3 重复操作符

重复操作符用于描述信号或事件在一段时间内重复出现的模式

2.3.1 [*n]操作符

语法: A [*n]
含义: A 必须连续出现 n 次。
特点: 用于描述信号在连续的 n 个时钟周期内保持不变。

property req_stable_for_n_cycles;@(posedge clk) req [*3];  // req 必须在 3 个连续的时钟周期内保持不变
endpropertyassert property (req_stable_for_n_cycles)else $error("Assertion failed: req_stable_for_n_cycles");

2.3.2 [->n]操作符

语法: A [->n]
含义: A 必须至少出现 n 次。
特点: 用于描述信号在一段时间内至少出现 n 次。

property req_at_least_n_times;@(posedge clk) req [->3];  // req 必须至少出现 3 次
endpropertyassert property (req_at_least_n_times)else $error("Assertion failed: req_at_least_n_times");

2.3.3 [=n]操作符

语法: A [=n]
含义: A 必须恰好出现 n 次。
特点: 用于描述信号在一段时间内恰好出现 n 次。

property req_exactly_n_times;@(posedge clk) req [=3];  // req 必须恰好出现 3 次
endpropertyassert property (req_exactly_n_times)else $error("Assertion failed: req_exactly_n_times");

2.3.4 [*]操作符

语法: A [*]
含义: A 必须一直保持不变。
特点: 用于描述信号在无限长的时间内保持不变。

property req_always_stable;@(posedge clk) req [*];  // req 必须一直保持不变
endpropertyassert property (req_always_stable)else $error("Assertion failed: req_always_stable");

2.3.5 [=0]操作符

语法: A [=0]
含义: A 不得出现。
特点: 用于描述信号在一段时间内不得出现。

property req_never_occurs;@(posedge clk) req [=0];  // req 不得出现
endpropertyassert property (req_never_occurs)else $error("Assertion failed: req_never_occurs");

2.3.6 [->0]操作符

语法: A [->0]
含义: A 可以出现也可以不出现。
特点: 用于描述信号在一段时间内可以出现也可以不出现。

property req_optional_occurrence;@(posedge clk) req [->0];  // req 可以出现也可以不出现
endpropertyassert property (req_optional_occurrence)else $error("Assertion failed: req_optional_occurrence");

上述操作符总结：

module sva_example (input wire clk,input wire rst_n,input wire req,input wire ack
);// 1. req 在 3 个连续的时钟周期内保持不变property req_stable_for_n_cycles;@(posedge clk) req [*3];endpropertyassert property (req_stable_for_n_cycles)else $error("Assertion failed: req_stable_for_n_cycles");// 2. req 至少出现 3 次property req_at_least_n_times;@(posedge clk) req [->3];endpropertyassert property (req_at_least_n_times)else $error("Assertion failed: req_at_least_n_times");// 3. req 恰好出现 3 次property req_exactly_n_times;@(posedge clk) req [=3];endpropertyassert property (req_exactly_n_times)else $error("Assertion failed: req_exactly_n_times");// 4. req 在无限长的时间内保持不变property req_always_stable;@(posedge clk) req [*];endpropertyassert property (req_always_stable)else $error("Assertion failed: req_always_stable");// 5. req 在无限长的时间内不断出现property req_infinite_occurrences;@(posedge clk) req [->*];endpropertyassert property (req_infinite_occurrences)else $error("Assertion failed: req_infinite_occurrences");// 6. req 不得出现property req_never_occurs;@(posedge clk) req [=0];endpropertyassert property (req_never_occurs)else $error("Assertion failed: req_never_occurs");// 7. req 可以出现也可以不出现property req_optional_occurrence;@(posedge clk) req [->0];endpropertyassert property (req_optional_occurrence)else $error("Assertion failed: req_optional_occurrence");endmodule

2.4 匹配操作符

匹配操作符用于描述和检查信号之间的匹配关系；

2.4.1 intersect操作符

语法: A intersect B
含义: A 和 B 必须在同一时钟周期内同时发生。
特点: 用于描述两个序列或事件在同一时钟周期内同时满足；

sequence req;req;
endsequencesequence ack;ack;
endsequenceproperty req_ack_intersect;@(posedge clk) req intersect ack;  // req 和 ack 必须在同一时钟周期内同时发生
endpropertyassert property (req_ack_intersect)else $error("Assertion failed: req_ack_intersect");

2.4.2 within操作符

语法: A within B
含义: A 必须在 B 发生的时间范围内发生。
特点: 用于描述一个序列 A 必须在另一个序列 B 的时间范围内发生。

sequence start;start;
endsequencesequence end;end;
endsequenceproperty start_within_end;@(posedge clk) start within end;  // start 必须在 end 发生的时间范围内发生
endpropertyassert property (start_within_end)else $error("Assertion failed: start_within_end");

2.4.3 throught操作符

语法: A throughout B
含义: A 必须在整个 B 发生的时间范围内一直成立。
特点: 用于描述一个序列 A 在另一个序列 B 的整个持续时间内都必须成立；

sequence active;active;
endsequencesequence busy;busy;
endsequenceproperty active_throughout_busy;@(posedge clk) active throughout busy;  // active 必须在整个 busy 发生的时间范围内一直成立
endpropertyassert property (active_throughout_busy)else $error("Assertion failed: active_throughout_busy");

2.4.4 before操作符

语法: A before B
含义: A 必须在 B 之前发生。
特点: 用于描述一个序列 A 必须在另一个序列 B 之前发生。

sequence setup;setup;
endsequencesequence start;start;
endsequenceproperty setup_before_start;@(posedge clk) setup before start;  // setup 必须在 start 之前发生
endpropertyassert property (setup_before_start)else $error("Assertion failed: setup_before_start");

2.4.5 first_match操作符

语法: first_match (A, B)
含义: A 和 B 中的第一个匹配项。
特点: 用于描述多个序列或事件中的第一个匹配项。

sequence event1;event1;
endsequencesequence event2;event2;
endsequenceproperty first_event;@(posedge clk) first_match(event1, event2);  // event1 和 event2 中的第一个匹配项
endpropertyassert property (first_event)else $error("Assertion failed: first_event");

2.4.6 s_next 操作符

语法: s_next(A, B)
含义: A 发生后，下一个时钟周期 B 必须发生。
特点: 用于描述 A 和 B 之间的严格时序关系。

sequence req;req;
endsequencesequence ack;ack;
endsequenceproperty req_s_next_ack;@(posedge clk) s_next(req, ack);  // req 发生后，下一个时钟周期 ack 必须发生
endpropertyassert property (req_s_next_ack)else $error("Assertion failed: req_s_next_ack");

上述匹配操作符代码：

module sva_example (input wire clk,input wire rst_n,input wire req,input wire ack,input wire busy
);// 1. req 和 ack 必须在同一时钟周期内同时发生property req_ack_intersect;@(posedge clk) req intersect ack;endpropertyassert property (req_ack_intersect)else $error("Assertion failed: req_ack_intersect");// 2. req 必须在 busy 发生的时间范围内发生property req_within_busy;@(posedge clk) req within busy;endpropertyassert property (req_within_busy)else $error("Assertion failed: req_within_busy");// 3. busy 在整个 req 发生的时间范围内一直成立property busy_throughout_req;@(posedge clk) busy throughout req;endpropertyassert property (busy_throughout_req)else $error("Assertion failed: busy_throughout_req");// 4. req 必须在 busy 之前发生property req_before_busy;@(posedge clk) req before busy;endpropertyassert property (req_before_busy)else $error("Assertion failed: req_before_busy");// 5. req 和 ack 中的第一个匹配项property first_event;@(posedge clk) first_match(req, ack);endpropertyassert property (first_event)else $error("Assertion failed: first_event");// 6. req 发生后，下一个时钟周期 ack 必须发生property req_s_next_ack;@(posedge clk) s_next(req, ack);endpropertyassert property (req_s_next_ack)else $error("Assertion failed: req_s_next_ack");endmodule

2.5 内键函数

2.5.1 $rose函数

property rose_signal;@(posedge clk) $rose(req) |-> ack;  // 如果 req 从 0 变为 1，则在当前时钟周期 ack 必须成立
endpropertyassert property (rose_signal)else $error("Assertion failed: rose_signal");

2.5.2 $fell

property fell_signal;@(posedge clk) $fell(req) |-> ack;  // 如果 req 从 1 变为 0，则在当前时钟周期 ack 必须成立
endpropertyassert property (fell_signal)else $error("Assertion failed: fell_signal");

2.5.3 $stable

property stable_signal;@(posedge clk) $stable(req) |-> ack;  // 如果 req 在前一个时钟周期没有变化，则在当前时钟周期 ack 必须成立
endpropertyassert property (stable_signal)else $error("Assertion failed: stable_signal");

2.5.4 $past

property past_value;@(posedge clk) $past(req, 8) |-> ack;  // 如果 req 在 8 个时钟周期前成立，则在当前时钟周期 ack 必须成立
endpropertyassert property (past_value)else $error("Assertion failed: past_value");

2.5.5 others

$onehot(); $onehot0(); $conutones();

3 FIFO空满断言

证的是一个深度为32的FIFO，通过利用读写两个counter去记录目前为止。一旦满了，cnt=32，full应该立即拉高。一旦为空，cnt=0，empty应该立即拉高。

//counter
reg [15:0] w_cnt,r_cnt;
wire [15:0] cnt;
always@(posedge wif.clk)beginif(~wif.rstn)w_cnt<=16'b0;else if(wif.en)w_cnt<=w_cnt+1;
end
always@(posedge rif.clk)beginif(~rif.rstn)r_cnt<=16'b0;else if(rif.en)r_cnt<=r_cnt+1;
end
//check current counter
assign cnt=w_cnt-r_cnt;//check full
property full_chk;@(posedge wif.clk) disable iff(~wif.rstn)cnt==32 && $rose(cnt[5]) |-> $rose(wif.valid);
endpropertya_full_chk: assert property(full_chk) $display("check full pass");else $display("ERROR: check full fail");
c_full_chk: cover property(full_chk);//check empty
property empty_chk;@(posedge rif.clk) disable iff(~rif.rstn)cnt==0 && $fell(cnt[0]) |-> $rose(rif.valid);
endpropertya_empty_chk: assert property(empty_chk) $display("check empty pass");else $display("ERROR: check empty fail");
c_empty_chk: cover property(empty_chk);

[ref]
1.https://blog.csdn.net/qq_29325189/article/details/131058187