使用 SVA，我们如何编写一个属性来检查我们没有同时收到两个 reqreq1 和 req2

问题描述

req1 和 req2 都是异步的。而且我想检查在模拟中的任何时候，req2 为真，而 req1 为真。我试过了

property not_req2_while_req1;
    @(negedge req1)
    1 |-> $stable(req2);
endproperty
ASSERT_NOT_REQ2_WHILE_REQ1:assert property (not_req2_while_req1);

但它似乎没有给出预期的结果。我在这里做错了什么？

解决方法

我不确定您是否正确表达了您的要求，因为您所写的内容甚至都没有表达出来，但以下 SVA 代码与您所说的相符。

ASSERT_NOT_REQ2_WHILE_REQ1: assert final (req1 -> !req2);

编辑： 您编辑了您的问题，只要求 req1 和 req2 永远不会同时为真。那是一个NAND操作

ASSERT_NAND_REQ2_REQ1: assert final ( !(req1&&req2) );