上两篇主要是讲述断言的概念，基本语法，总结等等
这一篇主要是以PPT的形式展示各个场景下关于断言的应用。
为了在设计中加入断言的功能，因此需要写一个DUT。如下：
`define true 1 `define free (a && b && c && d) module assertion( input clk, input rst_n ); reg a = 1'b0 ; reg b = 1'b0 ; reg c = 1'b0 ; reg d = 1'b0 ; reg e = 1'b0 ; reg f = 1'b0 ; reg start = 1'b0 ; reg stop = 1'b0 ; always @(posedge clk) begin a <= $urandom_range(0,1); b <= $urandom_range(0,1); c <= $urandom_range(0,1); d <= $urandom_range(0,1); e <= $urandom_range(0,1); f <= $urandom_range(0,1); start <= $urandom_range(0,1); stop <= $urandom_range(0,1); end assign state = {a,b,c,d}; assign bus = {a,b,c,d}; `ifdef SIM_ASSERTION_ON //a1 sequence s1; @(posedge clk) a; endsequence property p1; s1; endproperty a1: assert property (p1); //a2 sequence s2; @(posedge clk) $rose(a); endsequence property p2; s2; endproperty a2: assert property (p2); //a3 property p3; @(posedge clk) a || b; endproperty a3: assert property (p3); //a4 sequence s4; @(posedge clk) a ##2 b; endsequence property p4; s4; endproperty a4: assert property (p4); //a5 property p5; @(posedge clk) a ##2 b; endproperty a5:assert property(p5); //a6 sequence s6; @(posedge clk) a ##2 b; endsequence property p6; not s6; endproperty a6: assert property(p6); //a7 property p7; @(posedge clk) a ##2 b; endproperty a7: assert property (p7) $display("Property p7 successed "); else $display("Property p7 failed "); //a8 property p8; @(posedge clk) a |-> b; endproperty a8: assert property (p8); //a9 property p9; @(posedge clk) a |=> b; endproperty a9: assert property (p9); //a10 property p10; @(posedge clk) a |-> ##2 b; endproperty a10: assert property (p10); //a11 sequence s11a; @(posedge clk)(a && b) ##1 c; endsequence sequence s11b; @(posedge clk) ##2 !d; endsequence property p11; s11a |-> s11b; endproperty a11: assert property (p11); //a12 property p12; @(posedge clk) ( a&&b ) |-> ## [1:3] c; endproperty a12: assert property (p12); //a13 property p13; @(posedge clk) ( a&&b ) |-> ## [0:2] c; endproperty a13: assert property (p13); //a14 property p14; @(posedge clk) a |-> ##[1:$] b ##[0:$] c; endproperty a14: assert property (p14); //a15 sequence s15a; @(posedge clk) a ##1 b; endsequence sequence s15b; @(posedge clk) c ##1 d; endsequence property p15a; s15a |=> s15b; endproperty property p15b; s15a.ended |-> ##2 s15b.ended; endproperty a15a: assert property (p15a); a15b: assert property (p15b); //a17 property p17; @(posedge clk) c ? d == a : d == b; endproperty a17: assert property(p17); //a18 sequence s18a; @(posedge clk) a ##1 b; endsequence sequence s18a_ext; @(posedge clk) a ##1 b ##1 `true; endsequence sequence s18b; @(posedge clk) c ##1 d; endsequence property p18; @(posedge clk) s18a.ended |-> ##2 s18b.ended; endproperty property p18_ext; @(posedge clk) s18a_ext.ended |-> ##2 s18b.ended; endproperty a18: assert property (p18); a18_ext: assert property (p18_ext); //a19 property p19; @(posedge clk) (c && d) |-> ($past((a&&b), 2) == 1'b1); endproperty a19: assert property (p19); //a20 property p20; @(posedge clk) (c && d) |-> ($past ( ( a&&b ), 2, e) == 1'b1); endproperty a20: assert property (p20); //a21 property p21; @(posedge clk) $rose(start) |-> ##2 (a[*3]) ##2 stop ##1 !stop ; endproperty a21: assert property (p21); //a22 property p22; @(posedge clk) $rose(start) |-> ##2 ((a ##2 b) [*3]) ##2 stop ; endproperty a22: assert property (p22); //a23 property p23; @(posedge clk) $rose(start) |-> ##2 ((a ##[1:4] b) [*3]) ##2 stop ; endproperty a23: assert property (p23); //a24 property p24; @(posedge clk) $rose(start) |-> ##2 (a [*1 : $]) ##1 stop ; endproperty a24: assert property (p24); //a25 property p25; @(posedge clk) $rose(start) |-> ##2 (a [->3]) ##1 stop ; endproperty a25: assert property (p25); //a26 property p26; @(posedge clk) $rose(start) |-> ##2 (a [=3]) ##1 stop ##1 !stop; endproperty a26: assert property (p26); //a27 sequence s27a; @(posedge clk) a ##[1:2] b; endsequence sequence s27b; @(posedge clk) c ##[2:3] d; endsequence property p27; @(posedge clk) s27a and s27b ; endproperty a27: assert property(p27); //a28 sequence s28a; @(posedge clk) a ##[1:2] b; endsequence sequence s28b; @(posedge clk) c ##[2:3] d; endsequence property p28; @(posedge clk) s28a intersect s28b ; endproperty a28: assert property(p28); //a29 sequence s29a; @(posedge clk) a ##[1:2] b; endsequence sequence s29b; @(posedge clk) c ##[2:3] d; endsequence property p29; @(posedge clk) s29a or s29b ; endproperty a29: assert property(p29); //a30 sequence s30a; @(posedge clk) a ##[1:3] b; endsequence sequence s30b; @(posedge clk) c ##[2:3] d; endsequence property p30; @(posedge clk) first_match (s30a or s30b) ; endproperty a30: assert property(p30); //a31 property p31; @(posedge clk) $fell(start) |-> (!start) throughout (##1 ( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) ); endproperty a31: assert property(p31); //a32 sequence s32a; @(posedge clk) (( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) ); endsequence sequence s32b; @(posedge clk) $fell(start) ## [5:10] $rose(start); endsequence sequence s32; @(posedge clk) s32a within s32b; endsequence property p32; @(posedge clk) $fell(start) |-> s32; endproperty a32: assert property(p32); //a33 a33a: assert property( @ (posedge clk) $onehot(state) ); a33b: assert property( @ (posedge clk) $onehot0(state) ); a33c: assert property( @ (posedge clk) $isunknown(bus) ); a33d: assert property( @ (posedge clk) $countones (bus) ); //a34 property p34; @(posedge clk) disable iff (rst_n) $rose (start) |-> a[=2] ##1 b[=2] ##1 !start ; endproperty //a35 property p35; (@(posedge clk) 1[*2:5] intersect(a ##[1:$] b ##[1:$] c)); endproperty a35: assert property(p35); //a36 property arb (a,b,c,d); @(posedge clk) ($fell (a) ##[2:5] $fell(b) ) |-> ##1 ($fell (c) && $fell(d) ) ## 0 (!c && !d) [*4] ##1 (c&&d) ##1 b; endproperty a36_1: assert property(arb(a1,b1,c1,d1)); a36_2: assert property(arb(a2,b2,c2,d2)); a36_3: assert property(arb(a3,b3,c3,d3)); //a37 property p_nest; @(posedge clk) $fell (a) |-> ##1 (!b && !c && !d ) |-> ## [6:10] `free; endproperty a_nest: assert property(p_nest); property p_nest1; @(posedge clk) $fell (a) ##1 (!b && !c && !d ) |-> ## [6:10] `free; endproperty a_nest1: assert property(p_nest1); //a_if_else property p_if_else; @(posedge clk) ($fell (start)##1(a || b))|-> if (a) (c[->2] ##1 e) else (d[->2] ##1 f); endproperty a_if_else: assert property(p_if_else); `endif endmodule
通过运行Makefile脚本，调用VCS以及Verdi命令来实现以及查看断言的波形。
总结如下：
目录
1、概述
2、断言的常用语法
3、断言的应用
至此，关于断言的知识点全部更新完全,有疑问的欢迎交流。