vhdl - 可变延迟流水线的 PSL 断言

Question

我正在尝试编写一个 PSL 断言来检查输入断言的数量是否与输出断言的数量相匹配。

例如:

.

在输入上任何时候都可能发生任何事情，输出也可以在任何时候断言。确切时间未知，也不重要。我要验证的是没有信息丢失。

我提出了以下 PSL 声明来验证这一点。这是一个强断言，意味着在测试结束时所有断言都需要“完成”。

assert always { input='1' |-> {[*] ; output='1'} }!;

例如，以下应该是失败但此 PSL 通过:

我注意到这个语句并不强，因为不同的输入断言可以被相同的输出断言匹配。例如:

实现这样的 PSL 的好方法是什么？显然我也可以通过其他方式验证它(计算输入和输出断言)但是有没有办法用 PSL 来做到这一点？是否有我可以使用 SVA 实现的等效检查？

Answer 1

我可能在这里遗漏了一些东西，但为什么不简单地实现计数器并在测试结束时比较它们呢？

always @(posedge clk) bgein
  if (reset) begin
    counter_in <= 0;
    counter_out <= 0;
  end else begin
    if (input_) counter_in++;
    if (output_) counter_out++;
  end
end 
final begin
  assert (counter_in == counter_out);
end

即使出现溢出，它仍然可以工作。