Утверждение 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

даже если вы переполнитесь, он все равно будет работать.