爱华网1. SVA的插入位置：在一个.v文件中： module ABC (); rtl 代码 SVA断言 endmodule
注意：不要将SVA写在enmodule外面。
2. 断言编写的一般格式是： 【例】 断言名称1：assertproperty(事件1) //没有分号 $display("........",$time); //有分号 else $display("........",$time); //有分号
断言名称2：assert property(事件2) $display("........",$time); else $display("........",$time);
断言的目的是：断定“事件1”和“事件2”会发生，如果发生了，就记录为pass，如果没发生，就记录为fail。注意：上例中没有if，只有else，断言本身就充当if的作用。
上例中，事件1和事件2可以用两种方式来写： (1)序列块：sequence name; 。。。。。。。。。; endsequence
(2) 属性块： propertyname; 。。。。。。。。。; endsequence
从定义来讲，sequence块用于定义一个事件（砖），而property块用于将事件组织起来，形成更复杂的一个过程（楼）。sequence块的内容不能为空，你写乱字符都行，但不能什么都没有。sequence也可以包含另一个sequence,如： sequences1; s2(a,b); endsequence //s1和s2都是sequence块
sequence块和property块都有name，使用assert调用时都是：“assert property(name);”在SVA中，sequence块一般用来定义组合逻辑断言，而property一般用来定义一个有时间观念的断言，它会常常调用sequence，一些时序操作如“|->”只能用于property就是这个原因。 注：以下介绍的SVA语法，既可以写在sequence中，也可以写在property中，语法是通用的。
3. 带参数的property、带参数的sequenceproperty也可以带参数，参数可以是事件或信号，调用时写成：assert property(p1(a,b))被主sequence调用的从sequence也能带参数，例如从sequence名字叫s2，主sequence名字叫s1: sequence s1; s2(a,b); endsequence
4. property内部可以定义局部变量，像正常的程序一样。 propertyp1; int cnt; ..................... endproperty
【注】在介绍语法之前，先强调写断言的一般格式： 一般，断言是基于时序逻辑的，单纯进行组合逻辑的断言很少见，因为太费内存（时序逻辑是每个时钟周期判断一次，而组合逻辑却是每个时钟周期内判断多次，内存吃不消）。 因此，写断言的一般规则是： time +event，要断定发生什么event，首先要指定发生event的时间，例如每个时钟上升沿 + 发生某事 某信号下降时 + 发生某事
5. 语法1：信号（或事件）间的“组合逻辑”关系：(1) 常见的有：&&, ||, !, ^(2)a和b哪个成立都行，但如果都成立，就认为是a成立：firstmatch(a||b)，与“||”基本相同，不同点是当a和b都成立时，认为a成立。(3) a ? b:c ———— a事件成功后，触发b，a不成功则触发c
6.语法2：在“时序逻辑”中判断独立的一根信号的行为： @ (posedge clk) A事件; ————当clk上升沿时，如果发生A事件，断言将报警。边沿触发内置函数：(假设存在一个信号a) $rose( a );———— 信号上升 $fell( a );———— 信号下降 $stable( a );———— 信号值不变
7.语法3：在“时序逻辑”中判断多个事件/信号的行为关系：(1) intersect(a,b)———— 断定a和b两个事件同时产生，且同时结束。(2) a within b ———— 断定b事件发生的时间段里包含a事件发生的时间段。(3) a ##2 b ———— 断定a事件发生后2个单位时间内b事件一定会发生。 a ##[1:3] b ———— 断定a事件发生后1~3个单位时间内b事件一定会发生。 a ##[3:$] b ———— 断定a事件发生后3个周期时间后b事件一定会发生。(4) c throughout (a ##2 b) ———— 断定在a事件成立到b事件成立的过程中，c事件“一直”成立。(5) @ (posedge clk) a |-> b ———— 断定clk上升沿后，a事件“开始发生”，同时，b事件发生。(6)@ (posedge clk) a.end |-> b————断定clk上升沿后，a事件执行了一段时间“结束”后，同时，b事件发生。 注："a|-> b" 在逻辑上是一个判断句式，即： if a b; else succeed;
因此，一旦 a发生，b 必须发生，断言才成功。如果a没发生，走else，同样成功。
(7)@ (posedge clk) a |=> b ———— 断定clk上
