systemverilog中的assertion用法整理
时序电路讲究建立时间、保持时间需要留有裕量。这也说明了，在电路中信号的顺序以及之间的时序关系十分重要
如果激励的输入输出不满足设计的要求，那么测试的结果也是不可靠的。同样，如果设计内部不满足要求，输入输出的关系也不正确。为了检验这之间的关系，便引入了assertion.
由参考资料可知几点，非时序逻辑时，assertion的形式如下：
assertion_test: assert (condition) else $error(check failed);而对于时序逻辑的assertion，形式如下:
assertion_test: assert property( @(posedge clk) disable iff (rst) condition ) else $error(check failed);或
property assertion_test: @(posedge clk) disable iff (rst) condition )endpropertyassertion_action: assert property (assertion_test)其它的一些系统函数，操作符作用如下，可以进参考资料查看：
那么，接下来我们就做个小测试，使用req ack的握手过程作为检测过程。
信号的时序图要求如上图，握手过程为：
req信号拉高，此时ack信号还是低电平在req信号拉高后，ack信号拉高req端检测到ack拉高，拉低req信号ack端的处理结束，检测到req信号拉低，ack信号拉低那么，我们简单写一个ack应答的模块，内容如下：
module req2ack( input clk , input rst , input en , input req , output reg ack );reg [7:0] req_arr;always @ (posedge clk or posedge rst)begin if (rst) req_arr <= 'd0; else if (en) req_arr <= {req_arr[5:0], {2{req}}};endalways @ (posedge clk or posedge rst)begin if (rst) ack <= 1'b1; else if (en) ack ##1 (req & ~ack)[*0:$] ##1 (req & ack) ) else $error(req to ack rising edge is fail);check_req_ack_fall: assert property( @(posedge clk) disable iff (rst) $rose(ack) |- > (req & ack)[*0:$] ##1 (~req & ack)[*0:$] ##1 (~req & ~ack) ) else $error(req to ack falling edge is fail);第一块内容，检查req-ack握手过程的1，2两步；第二块内容，检查req-ack握手过程的3，4步。
$rose(req)的意思是由上文或参考资料可知，等到req信号的上升沿有效；
|->操作符表示，lhs(左侧表达式)条件满足，则在同一时刻去检查rhs的表达式；
##1 代表延时1个时钟周期；
(req & ~ ack)[*0:$] 代表此时req信号为高，ack信号为低的情况满足0或多个时钟周期；周期不确定
第一块内容的意思是，等到req信号上升沿，过一个时钟周期检查req拉高，ack为低的情况是否满足，这个过程可能持续多个周期，不确定；然后就是ack信号拉高。检查结束
第二块内容的意思是，等到ack信号上升沿，检查req和ack的信号是否都拉高，这个过程可能持续多个周期，不确定；然后req信号拉低，ack保持，也会持续多个周期，最后ack信号也拉低。
最后，在运行vcs时，需要加入“+fsdb+sva_success -assert”
测试结果：
那么，我们对激励稍作修改下：
initial begin clk = 0; rst = 1; en = 0; req = 0; #100 rst = 0; en = 1; #100 req = 1; wait(ack); #20 req = 0; wait(~ack); #50 $finish;endassertion的结果：
这只是作为一个小例子，而且写的过于匆忙，我相信应该是有更好的assertion写法，所以权当是一次记录的草稿内容。
非车载充电机是什么
美光发布面向汽车的内存 洲明科技LED巨幕助力打造沉浸式大会
光峰科技率先采用中国CVIA亮度新标 ALPD高亮破局而出
宽动态范围高性能电能计量芯片IDT90E2X
浅谈剩余电流动作断路器在钢铁厂供电系统改造中的应用
systemverilog中的assertion用法整理
区块链赋能供应链金融意味着什么
STM32单片机的ISP、IAP、ICP三种烧录方式
关于PCB材料参数的提取的介绍
LG未来会将摄像头集成到智能手表中
【触觉智能 Purple Pi OH 开发板体验】+ Linux下位移运算及实现
国美零售与中国电信联合打造的5G家居体验厅，实现了5G信号的覆盖
Microchip推出低功耗耐辐射（RT）PolarFire FPGA，助力客户以更低的系统总成本实现高带宽空间系统
海格通信与麒麟软件签订战略合作协议共建“芯片+操作系统”
ePTFE送话器防水膜材料助力实现IP68防尘防水标准
2010年十大尖端科技揭晓
用于调频收音机的有源天线放大器电路图
苹果发布2018年第三财季业绩报告,iPhone X是全球最畅销的iPhone机型
解决EMI传导干扰7个对策解析
什么叫GPRS
如果激励的输入输出不满足设计的要求，那么测试的结果也是不可靠的。同样，如果设计内部不满足要求，输入输出的关系也不正确。为了检验这之间的关系，便引入了assertion.
由参考资料可知几点，非时序逻辑时，assertion的形式如下：
assertion_test: assert (condition) else $error(check failed);而对于时序逻辑的assertion，形式如下:
assertion_test: assert property( @(posedge clk) disable iff (rst) condition ) else $error(check failed);或
property assertion_test: @(posedge clk) disable iff (rst) condition )endpropertyassertion_action: assert property (assertion_test)其它的一些系统函数，操作符作用如下，可以进参考资料查看：
那么，接下来我们就做个小测试，使用req ack的握手过程作为检测过程。
信号的时序图要求如上图，握手过程为：
req信号拉高，此时ack信号还是低电平在req信号拉高后，ack信号拉高req端检测到ack拉高，拉低req信号ack端的处理结束，检测到req信号拉低，ack信号拉低那么，我们简单写一个ack应答的模块，内容如下：
module req2ack( input clk , input rst , input en , input req , output reg ack );reg [7:0] req_arr;always @ (posedge clk or posedge rst)begin if (rst) req_arr <= 'd0; else if (en) req_arr <= {req_arr[5:0], {2{req}}};endalways @ (posedge clk or posedge rst)begin if (rst) ack <= 1'b1; else if (en) ack ##1 (req & ~ack)[*0:$] ##1 (req & ack) ) else $error(req to ack rising edge is fail);check_req_ack_fall: assert property( @(posedge clk) disable iff (rst) $rose(ack) |- > (req & ack)[*0:$] ##1 (~req & ack)[*0:$] ##1 (~req & ~ack) ) else $error(req to ack falling edge is fail);第一块内容，检查req-ack握手过程的1，2两步；第二块内容，检查req-ack握手过程的3，4步。
$rose(req)的意思是由上文或参考资料可知，等到req信号的上升沿有效；
|->操作符表示，lhs(左侧表达式)条件满足，则在同一时刻去检查rhs的表达式；
##1 代表延时1个时钟周期；
(req & ~ ack)[*0:$] 代表此时req信号为高，ack信号为低的情况满足0或多个时钟周期；周期不确定
第一块内容的意思是，等到req信号上升沿，过一个时钟周期检查req拉高，ack为低的情况是否满足，这个过程可能持续多个周期，不确定；然后就是ack信号拉高。检查结束
第二块内容的意思是，等到ack信号上升沿，检查req和ack的信号是否都拉高，这个过程可能持续多个周期，不确定；然后req信号拉低，ack保持，也会持续多个周期，最后ack信号也拉低。
最后，在运行vcs时，需要加入“+fsdb+sva_success -assert”
测试结果：
那么，我们对激励稍作修改下：
initial begin clk = 0; rst = 1; en = 0; req = 0; #100 rst = 0; en = 1; #100 req = 1; wait(ack); #20 req = 0; wait(~ack); #50 $finish;endassertion的结果：
这只是作为一个小例子，而且写的过于匆忙，我相信应该是有更好的assertion写法，所以权当是一次记录的草稿内容。
非车载充电机是什么
美光发布面向汽车的内存 洲明科技LED巨幕助力打造沉浸式大会
光峰科技率先采用中国CVIA亮度新标 ALPD高亮破局而出
宽动态范围高性能电能计量芯片IDT90E2X
浅谈剩余电流动作断路器在钢铁厂供电系统改造中的应用
systemverilog中的assertion用法整理
区块链赋能供应链金融意味着什么
STM32单片机的ISP、IAP、ICP三种烧录方式
关于PCB材料参数的提取的介绍
LG未来会将摄像头集成到智能手表中
【触觉智能 Purple Pi OH 开发板体验】+ Linux下位移运算及实现
国美零售与中国电信联合打造的5G家居体验厅，实现了5G信号的覆盖
Microchip推出低功耗耐辐射（RT）PolarFire FPGA，助力客户以更低的系统总成本实现高带宽空间系统
海格通信与麒麟软件签订战略合作协议共建“芯片+操作系统”
ePTFE送话器防水膜材料助力实现IP68防尘防水标准
2010年十大尖端科技揭晓
用于调频收音机的有源天线放大器电路图
苹果发布2018年第三财季业绩报告,iPhone X是全球最畅销的iPhone机型
解决EMI传导干扰7个对策解析
什么叫GPRS