4

我有一个关于 PSL 断言的有趣问题。这是一个VHDL监控程序。这是一个专用于断言的过程，因此是一个不可综合的过程。此监视器检查当前 FSM 状态并存储两个寄存器的值：“ input1”和“ reg136”。最后，它触发一个“ assert”语句来比较这些寄存器的值。

process (clk)
  variable var_a : signed(7 downto 0);
  variable var_b : signed(7 downto 0);
begin
  if (rising_edge(clk)) then
    case state is
      when s0 =>
        var_a := signed(input1);
      when s22 =>
        var_t34 := signed(reg136);
      when s85 =>
        assert (var_t34 < var_a)
          report "Assertion xxx failed : (t34 < a)";
    end case;
  end if;
end process;

问题是：有没有办法将此监视器转换为 PSL（属性规范语言）断言？

重要提示：寄存器“input1”和“reg136”只能在 fsm 状态分别处于状态 s0 和 s22 时读取。否则，这些寄存器中包含的数据不属于断言变量“a”和“t34”。因此，PSL 语句需要一种方法来读取和存储正确 fsm 状态的值。

谢谢 ！

4

1 回答 1

0

实际上，我想我找到了一种使用prevPSL 功能的方法。

始终断言 (state = s85) -> (prev(reg136, 85-22) < prev(input1, 85-0)) @rising_edge(clk)

它要求 fsm 在每个时钟周期将其状态寄存器递增 1，或者知道从状态 s0 或 s22 到状态 s85 需要多少个时钟周期。

有人可以确认这会起作用吗？我没有准备好 PSL 的模拟器来检查这个...

于 2010-07-28T14:31:58.403 回答