SV 断言问题

L_2023 · 发表于 2023-7-19 10:21:15

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

最近做ahb to apb bridge验证时，遇到一个断言问题，在这里请教一下大家。

断言写在apb slave interface里面的，下图是代码

登录/注册后可看大图

断言检查：PSELx上升沿后的下一个周期，PENABLE也跳变为高

仿真波形

登录/注册后可看大图

断言结果

登录/注册后可看大图

从波形上看PSELx上升沿后的下一个周期，PENABLE确实跳变为高了，但为什么会断言失败了？这与断言的采样有关系吗？

xuehao94 · 发表于 2023-7-20 10:08:13

对于@(posedge clk) a #2 b这样的属性，它在每个时钟上升沿检查信号"a" 是否为高。寻找是否为一个断言的有效开始。

如果信号"a"在给定的任何时钟上升沿不为高，检验器将产生一个错误信息。这并不是一个有效的错误信息因为我们不只关心a,更加关心a和b的关系。这个错误只表明这个时钟周期没有得到有效起始点。它们会在一段时间内产生大量的错误信息。

基于以上问题，SVA提供了蕴含操作。
蕴含等效于一个if-then结构。蕴含的左边叫作“先行算子”，右边叫作"后续算子”。当先行算子成功时，后续算子才会被计算。如果先行算子不成功，那么整个属性就默认地被认为成功。这叫作"空成功”
蕴含结构只能被用在属性定义中，不能在序列中使用。

蕴含分为两类：交叠蕴含和非交叠蕴含。

原文链接：https://blog.csdn.net/qq_41360172/article/details/127710438

became_an_icer · 发表于 2023-7-20 16:42:09

你改成
$rose(PSELx)##1 PENABLE
就正确了，你试试

L_2023 · 发表于 2023-7-20 19:49:23

became_an_icer 发表于 2023-7-20 16:42
你改成
$rose(PSELx)##1 PENABLE
就正确了，你试试

改成这个还是断言失败，看了楼上大佬的回复，改成$rose(PSELx) |=> $rose(PENABLE)成功了

L_2023 · 发表于 2023-7-20 19:51:02

xuehao94 发表于 2023-7-20 10:08
对于@(posedge clk) a #2 b这样的属性，它在每个时钟上升沿检查信号"a" 是否为高。寻找是否为一个断言的有 ...

感谢！改成$rose(PSELx) |=> $rose(PENABLE)成功了

[求助] SV 断言问题

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

站长推荐 /2