关于一个断言能不能用多个蕴含符

断言的蕴含符

背景

前段时间在学习断言的时候突然发现从来没有见过一个断言里有多个蕴含符的操作，于是找了一下资料。

核心内容

我的理解

结论是可以用多个蕴含符，但是不要这么干。

假设我们写了这么一条断言：

property check_abcd;
@(posedge clk) diable iff (rst_n)
a |-> b |-> c |-> d
endproperty

按照我们正常的思路，我希望看到的是a=1的时候bcd同时等于1，这条断言才算通过，但是实际上在连续蕴含符上，断言的逻辑是右结合，我们可以理解为实际上断言是这么解析上面这条断言的

property check_abcd;
@(posedge clk) diable iff (rst_n)
a |-> （b |-> （c |-> d））
endproperty

这就意味着，当a=1的时候，断言先检查c |-> d（我们暂时称这个结果为e）是否成立，然后检查b |-> e（我们暂时称这个结果为f）是否成立，最后检查a |-> f是否成立。于是这个条断言的结果就变成了下面这个表

断言结果从我们以为的只有一个场景会成功，变成了只有一个场景会失败。这还只是我用了最简单的连续蕴含符，如果断言的内容更加复杂，多蕴含符debug的难度也会直线上升。

规避这个问题我认为有两个方法，一个是用括号来分组，但是这种方法的问题就是在代码量较大的断言中可读性变得相对较差；还有一种方法就是用##0来替代|->，然后用sequence封装不含蕴含符的定义，让整个property种只有一个蕴含符。

实战要点

• 工作中可以这么用：不要使用多个蕴含符，用##0替代
• 容易踩的坑：sequence里不能用蕴含符

一句话总结

不要使用多个蕴含符，否则debug会很艰难