Перевод монитора VHDL в утверждение PSL - PullRequest
Новая
       25

Перевод монитора VHDL в утверждение PSL

4 голосов
/ 28 июля 2010

У меня есть интересный вопрос об утверждении 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.

Спасибо!

1 Ответ

0 голосов
/ 28 июля 2010

На самом деле, я думаю, что нашел способ сделать это с помощью функции prev PSL.

всегда утверждать (state = s85) -> (prev (reg136, 85-22)

Требуется, чтобы fsm увеличивал свой регистр состояния на единицу в каждом такте или знал, сколько тактов необходимо для перехода из состояния s0 или s22 в состояние s85.

Может кто-нибудь подтвердить, что это будет работать? У меня нет PSL-готового симулятора, чтобы проверить это ...

...