假设我们有一个协议,说明如下。一旦主设备将req
设置为fill
,从设备将通过rsp
发出4次传输信号:
整个事务的SVA序列将是(假设从属设备可以在idle
周期之间插入trans
周期):
req == fill ##1 (trans [->1]) [*4];
现在,假设允许主服务器传递请求。这意味着允许下一个fill
在4个trans
循环完成之前开始:
来自上面的SVA序列无济于事,因为对于第二个fill
,它将错误地匹配4个trans
周期,留下最后的trans
“浮动”。只有在之前的trans
匹配之后,才需要开始匹配fill
周期。
该序列需要在单个评估中不可用的全局信息。基本上它需要知道它的另一个实例正在运行。我能想到实现这个的唯一方法是使用一些RTL支持代码:
int num_trans_seen;
bit trans_ongoing;
bit trans_done;
bit trans_queued;
always @(posedge clk or negedge rst_n)
if (!rst_n) begin
num_trans_seen;
trans_ongoing <= 0;
trans_done <= 0;
trans_queued <= 0;
end
else begin
if (trans_ongoing)
if (num_trans_seen == 3 && req == trans) begin
trans_done <= 1;
if (req == fill || trans_queued)
trans_queued <= 0;
else
trans_ongoing <= 0;
num_trans_seen == 0;
end
else
if (trans_queued) begin
trans_queued <= 0;
trans_ongoing <= 1;
end
if (trans_done)
trans_done <= 0;
end
当事务正在进行时,上面的代码应该提高trans_ongoing
位,并且当发送trans_done
的最后一个trans
时,在时钟周期中脉冲fill
。 (我说应该因为我没有测试它,但这不是重点。让我们假设它有效。)
有这样的东西,可以重写序列:
req == fill ##0 (trans_ongoing ##0 trans_done [->1]) [*0:1]
##1 (trans [->1]) [*4];
这应该有效,但我对我需要支持代码的事实并不特别激动。它有很多冗余,因为我基本上重新描述了交易的一大部分以及流水线的工作原理。它也不是那么容易重复使用。可以将sequence
放入包中并在其他地方导入。支持代码只能放在某个模块中并重用,但它与存储序列的包是不同的逻辑实体。
这里的问题是:有没有办法编写流水线版本的序列,同时避免需要支持代码?
看起来rsp在反式启动之前总是处于空闲状态。如果rsp的idle
是一个常数值,并且它是trans
永远不会的值,那么你可以使用:
req == fill ##0 (rsp==idle)[->1] ##1 trans[*4];
当管道支持1到3个阶段时,上述情况应该有效。
对于4+深的管道,我认为你需要一些辅助代码。断言的成功/失败块可用于无法完成trans
的计数;这样可以避免编写额外的RTL。属性中的局部变量可用于对填充的计数值进行采样。采样值将用作开始对预期的反式模式进行采样的标准。
int fill_req;
int trans_rsp;
always @(posedge clk, negedge rst_n) begin
if(!rst_n) begin
fill_req <= '0;
trans_rsp <= '0;
end
else begin
if(req == fill) begin
fill_req <= fill_req + 1; // Non-blocking to prevent risk of race condition
end
end
end
property fill_trans();
int id;
@(posedge clk) disable iff(!rst_n)
(req == fill, id = fill_req) |-> (rsp==idle && id==trans_rsp)[->1] ##1 trans[*4];
endproperty
assert property (fill_trans()) begin
// SUCCESS
trans_rsp <= trans_rsp + 1; // Non-blocking to prevent risk of race condition
end
else begin
// FAIL
// trans_rsp <= trans_rsp + 1; // Optional for supporting pass after fail
$error("...");
end
仅供参考:我没有时间对此进行全面测试。它应该至少让你朝着正确的方向前进。
我进行了一些实验,找到了一个可能更符合您自己喜欢的解决方案;没有支持代码。
相当于trans[->4]
是(!trans[*] ##1 trans)[*4]
每IEEE Std 1800-2012§16.9.2重复序列。因此,我们可以使用局部变量来检测具有扩展形式的新填充请求。例如以下顺序
sequence fill_trans;
int cnt; // local variable
@(posedge clk)
(req==FILL,cnt=4) ##1 ( // initial request set to 4
(rsp!=TRANS,cnt+=4*(req==FILL))[*] // add 4 if new request
##1 (rsp==TRANS,cnt+=4*(req==FILL)-1) // add 4 if new request, always minus 1
)[*] ##1 (cnt==0); // sequence ends when cnt is zero
endsequence
除非没有提到另一个限定符,否则不能使用典型的assert property();
,因为每次有填充请求时它都会启动新的断言线程。而是使用expect
语句,它允许等待属性评估(IEEE Std 1800-2012§16.17Expect语句)。
always @(posedge clk) begin
if(req==FILL) begin
expect(fill_trans);
end
end
我尝试重新创建你的描述行为来测试https://www.edaplayground.com/x/5QLs
使用如下两个断言可以实现一种可能的解决方案。
第一张图片 -
(req == fill) && (rsp == idle) |=> ((rsp == trans)[->1])[*4]
第二张图片 -
(req == fill) && (rsp == trans) |=> ((rsp == trans)[->1])[*0:4] ##1 (rsp == idle) ##1 ((rsp == trans)[->1])[*4]
一个问题是,如果每个周期都有连续的“填充”请求(连续4次“填充”请求,没有任何中间“空闲”),那么第二个断言将不计算每个“填充”请求的“反向”周期(而是它只能在第二组“反式”循环中完成。
到目前为止,我无法修改给定bug的断言。