Assertion PSL pour un pipeline à retard variable

Question

J'essaie d'écrire une assertion PSL qui vérifie que le nombre d'assertions à l'entrée correspond au nombre d'assertions à la sortie.

Par exemple :

.

Sur l'entrée, tout peut arriver à tout moment et la sortie peut être activée à tout moment également. L'heure exacte est inconnue et n'est pas non plus importante. Ce que je veux vérifier, c'est qu'aucune information n'est perdue.

J'ai trouvé la déclaration PSL suivante pour le vérifier. Il s'agit d'une assertion forte, ce qui signifie qu'à la fin d'un test, toutes les assertions doivent avoir été "complétées".

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

Par exemple, ce qui suit devrait être un échec mais cette LSP est acceptée :

J'ai remarqué que cette affirmation n'est pas forte car des assertions d'entrée différentes peuvent correspondre à la même assertion de sortie. Par exemple :

Quelle serait la meilleure façon de mettre en œuvre une telle LSP ? Évidemment, je peux aussi le vérifier par d'autres moyens (en comptant les assertions d'entrée et de sortie) mais y aurait-il un moyen de le faire avec PSL ? Existe-t-il une vérification équivalente que je pourrais mettre en œuvre en utilisant SVA ?

Answer 1

J'ai peut-être raté quelque chose ici, mais pourquoi ne pas simplement mettre en place des compteurs et les comparer à la fin du test ?

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

même si vous obtenez un débordement, cela fonctionnera toujours.