首页 > 代码库 > Concurrent Assertion

Concurrent Assertion

Concurrent assertion中要求必须有clock,从而保证在每个clock edge都进行触发判断。

assertion与design进行同步执行,concurrent assert只能定义在module中。

每次concurrent assertion条件满足时,都会新开一个thread,所以最终的assert的执行时 multi-thread的。

关键字是 assert property()

一般在property中定义clock,以及sequence的触发条件,而在sequence中指定义signal的判断。

 

技术分享

 

assert与verilog的执行区间:

assert在当前time slot的rtl执行前,sample 上一个time slot的rtl的值,在observe region进行assert的计算判断。

在sample和compute之间会不会间隔一个时钟,主要靠操作符"|->"和“|=>”来决定。

 

技术分享

 

一般情况下,clock的定义直接放在property中,而保证sequence独立于时钟比较好,

对于比较复杂的assert,可以单独定义一个clocking block,来作为property的clock基准。

技术分享

对于一个大的design中,可能会有很多的assert在不同的module中,可以在某一个

assert中声明某个clocking block

技术分享

 

在assertion中可以传递参数,来保证复用性:

技术分享

也可以进行default的设置:

技术分享

 

在不需要property继续检查的场景,可以通过加disable iff + COND来看,

disable iff只能应用在property中,不能用在sequence,一般放在@posedge clock前边。

技术分享

 

sequence和property虽然都可以放clock event,但是推荐在property中实现。

sequence中不能有|->这样的操作符

Concurrent Assertion