1. assertion statement

Assertion statement有以下几种类型：

• assert: 指定DUT的property，必须要verify
• assume: 给验证环境指定假设的property。simulator检查这些property，但是formal工具会使用这些信息来产生输入激励。
• cover: 监控property评估的coverage
• restrict: 用于指定property是formal验证的constraint，simulation不需要检查该property。

assertions又可以分为两大类：concurrentandimmediate。Immediate assertion就像是procedural block中使用的statement，主要目的是用于simulation，并没有restrict的assertion statement。Concurrent assertions基于clock来的。

2. Immediate assertions

Immediate assertion可以用在procedural statement能执行的任何地方。它和if(expression)里的expression求解一样，如果expression为x/z/0，那么会被翻译为false，并且assertion statement判断为fail。反之，expression会被翻译为true，因此assertionstatement会pass的。有两种模式的immediate assertion：simple immediate assertions和deferred immediate assertions。在simple immediate assertion中，pass或fail在基于assertion evaluation时立马发生。在deferred immediate assertion中，action会被delay到time step的后期，用于防止一些毛刺之类的。

Immediate assertion的执行可以通过system task的assertion control来控制的。

Immediate assertion statement有immediate assert、immediate assume或immediate cover。

对于immediate assert statement来说，fail的话只是requirement的违例，可能存在bug。付过assert statement失败，且没有else分支，那么工具应该默认调用$error，除非$assertcontrol里control_type=9，把error抑制掉。

Deferred assertion有两种类型：observed deferred immediate assertions和final deferred immediate assertions。

3. concurrent assertions

Concurrent assertions用于描述时间跨越的行为，不像immediate assertions，它时基于clock进行的，因此concurrent assertion只会在出现clock tick时才会evaluated的。

Concurrent assertions在observed region会被evaluated求值评估的。

Concurrent assertion的expression里的value采样称为sampled value。在大多数情况下，sampled value是在preponed region进行的，但有几个重要的例外：

关键字property是区分immediate assertion和concurrent assertion的关键。

4. declaring sequence

一个命名的sequence可以在以下声明：

5. sequence operations

操作符的优先级如下：

6. sampled value functions

Sampled value functions可以用于访问一个expression的sampled values。这些functions可以访问sampled values、访问过去的sampled value、检测expression的sampled value的变化。Local variables和sequence方法matched不能用在这些functions的argument expressions。这些functions为：

这些functions其实不只是限制于assertion features，它们也可能用于proceduralcode。

之所以引入$sampled()函数，原因如下：

$rose、$fell、$stable、$changed这些value change functions用于检测sampled value的变化，它们执行的结果遵循如下规则：

— $rose returns true if the LSB of the expression changed to 1. Otherwise, it returns false.

— $fell returns true if the LSB of the expression changed to 0. Otherwise, it returns false.

— $stable returns true if the value of the expression did not change. Otherwise, it returns false.

— $changed returns true if the value of the expression changed. Otherwise, it returns false.

$past函数可以用于采样过去的值。它有以下三个可选的arguments：

— expression2 is used as a gating expression for the clocking event.

— number_of_ticks specifies the number of clock ticks in the past.

— clocking_event specifies the clocking event for sampling expression1.

7. declaring properties

property定义了design的一个行为。一个命名的property可以作为assumption、oligation、coverage specification来验证。验证为了使用这些行为，可以用assert、assume、cover statement。property的定义不产生任何的结果。

sequence和property操作符优先级和关联如下：

8. concurrent assertions

property本身永远不会求值去检查一个expression。它应该用在assertion statement内部来达到这种效果。一个concurrent assertion statement可以在以下指定：

Assertion statement的还行可以通过assertion control system tasks来控制的。

9. assert statement

Assert statement用于实施property。当assert statement评估为true时，pass statement的block会被执行。当assert statement评估为false，failed statement的block会被执行。当assert statement的property评估为disabled，没有action block会被执行，fail和pass statement的执行可以通过assertion action control task来控制的。如果没有action statement的话，一个null statement将会指定。如果没有action statement指定到else分支的话，在assertion fail的时候$error将会执行。

Action block不应该包含concurrent assert、assume、cover statement。但是，可以包含immediate assertion statements。

Assert statement的pass和fail statement是在reactive region执行的。

Assert statement例子如下：

10. assume statement

Assume statement的目的是允许properties被认为是formal analysis和dynamic simulation tools的assumptions(假设)。当一个property被assumed时，tools会约束环境来保证属性不变。

Formal analysis没有义务验证assumed properties是否成立。一个assumed property可以被认为时用来证明asserted properties。对于simulation来说，必须对环境进行约束，以便assume的属性保持不变。与assert properties一样，如果assume statement不能成立，那么必须检查并报告它。

11. cover statement

存在两类的cover statements：cover sequence和cover property。Cover sequence statement指定sequence coverage，cover property statement指定property coverage。两者的不同在于：sequence coverage对于每次评估到所有匹配的都会报告，但是property coverage的coverage count在每一次评估至多是增加一次。Cover statement是可以可选的pass statement（在reactive region执行的），pass statement不能保持呢任何concurrent assert、assume或cover statement。

12. restrict statement

在formal验证中，为了将tool约束到一个确定state，也可以使用restrict property。它和assume property有相同的semantics，但是restrict property statement在simulation时不会被验证，而且没有actionblock。

13. Using concurrent assertion statements outside procedural code

Concurrent assertion statement可以用于procedural context之外，例如位于module、interface或program。Concurrent assertion statement有assert、assume、cover或restrict statement。这样的concurrent statement使用always，这意味它指定新的evaluation在每一次它的clock event。

14. disable iff resolution

Default disable iff可以在generate block、module、interface、program里面定义。它提供了默认的disable条件给所有concurrent assertions在当前scope或subscope。进一步说，defualt可以扩展到任何nested module、interface、program、generateblock定义里。但如果nested里面有自己地鞥一的disable iff，那么外部的disable iff不生效。

在上述例子里，default disable iff作用于a1和a2。

15. clock resolution

有许多方式可以给property提供clock，有如下：

16. expect statement

Expect statement是一个procedural blocking statement，它允许等待property evaluation。语法如下：

Expect statement接受同样的语法去assert一个property。Expect statement会导致执行线程被block，直到给定的property是成功或者失败的。在expect后面的statement在observed region(所有的property完成evaluation)之后才会继续执行的。

Expect statement可以出现在任何wait statement可以出现的地方。

17. Clocking blocks and concurrent assertions

如果用于concurrent assertion的变量是clocking block变量，那么它只会在clocking block里被sampled的。