Tengo una especificación de la siguiente manera:
"Verifique que 'valido' no esté confirmado cuando 'validi = 1' solo para dos, uno o cero ciclos de clk consecutivos."
la siguiente afirmación FALLA (n-3 veces) en una secuencia de 111..1:
assert property (@(posedge clk) disable iff (rst) validi[*0:2] |=> !valido);
Supongo que el problema está en mi propiedad, ya que no cubre el caso de secuencias superpuestas (?). ¿Hay alguna forma de escribir una propiedad que se comporte bien?
Su afirmación comprueba si valido es BAJO cuando validi es ALTO durante tres ciclos de reloj consecutivos, por lo que es incorrecto. No funcionará incluso si cambias la condición de activación a validi[*0:1] debido a las secuencias superpuestas como lo has adivinado.
No tengo una solución en ese estilo de codificación, pero se puede crear una solución usando $past similar a la de la Academia de verificación * .
assert property (@(posedge clk) disable iff (rst)
($past(!validi, 0) ||
$past(!validi, 1) ||
$past(!validi, 2)) |=> !valido);
Ahora, la afirmación espera que valido sea BAJO si validi es BAJO en al menos uno de los últimos tres ciclos de reloj.
Lea otras preguntas en las etiquetas system-verilog