Abstract:介绍了一些OVL断言的语句
Introduction:此文为读 《Verilog Digital System Design-Register Transfer Level Synthsis,Testbench,and Verification》的笔记
Body:
1.断言验证的优点：
1>方便对程序进行测试，相比普通的testbench而言可提高测试的自动化
2>增加验证的可读性。
3>被正式的验证TOOL认可。
4>设计描述与测试过程包含在一个module块中。
2.断言的一般格式：
assert_name
#(static_parameters)
instance_name
(dynamic_arguments); //注意分号别忘记，下面的例子省去了
3.一些常用语句：
1>assert_always
#(severity_level,property_type,msg,coverage_level)
instance_name(clk,reset_n,test_expr)
始终验证：test_expr,已确保它在指定的时钟沿(clk表示上升沿，~clk表示下降沿)
上为true。若不正确，
则报警并且显示msg.
若reset_n为1'b1，则表示assertion monitor始终active.
2>assert_change
#(severity_level,width,num_cks,action_on_new_start,
property_type,msg,coverage_level)
instance_name(clk,reset_n,start_event,test_expr)
验证：start_event之后给定的时钟数（num_cks）内,tset_expr变化。
width表示test_expr的位宽，num_cks表示num_cks个时钟周期后，test_exps变化。
3>assert_one_hot
#(severity_level,width,property_type,msg,coverage_level)
instance_name(clk,reset_n,test_expr)
验证：当monitor激活时,n位test_expr中只有一位是1.
width表示test_expr的位宽。
例：可在设计描述中加入辅助逻辑来监测
reg [3:0] old;
always @(posedge clk)old<=q;
(因为为非阻塞赋值，所以下一个时钟周期把旧值赋给old,q为新值)
assert_one_hot #(1,4,0,"Err:Not Gray",0)
AOH(~clk,~rst,(old^q));
4>assert_cycle_sequence
#(severity_level,num_cks,necessary_condition,
property_type,msg,coverage_level)
instance_name(clk,reset_n,event_sequence)
验证：在给定的时钟周期，一系列事件的发生。
necessary_condition为0时验证：在指定的序列中，如果前面所有的状态
到达，最后的状态是否到达；
为1时验证：如果第一个状态到达，其后所有的状态是否到达。
5>assert_next
#(severity_level,num_cks,necessary_condition,
property_type,msg,coverage_level)
instance_name(clk,reset_n,start_event,test_expr)
验证：从开始到指定的时钟周期内，test_expr是否发生。
6>assert_implication
#(severity_level,property_type,msg,coverage_level)
instance_name(clk,reset_n,antecedent_expr,consequence_expr)
验证：在指定的时钟沿antecedent_expr是否正确，若是，则再验证
consequence_expr是否正确。
7>assert_no_overflow
#(severity_level,width,min,max,
property_type,msg,coverage_level)
instance_name(clk,reset_n,test_expr)
验证：test_expr是否为有效状态（有的状态编码不会用到所有状态）
width表示被测变量（通常为当前状态）的位宽，min,max表示状态的最大
、最小值。