Si “a” es “1” entonces “b” debe de ser “1”
assert property (@(negedge clk) a |-> b)
El concepto de implicación en las aserciones es una especie de condición de habilitación de las mismas. Si en un negedge clk la señal a no está igual a 1, la aserción no está habilitada y por tanto no puede fallar
¿Alternativas sin fallo?
- Pues si la aserción no esta habilitada: a=0 (independientemente de cómo esté b)
- Si la aserción está habilitada y la condición de la aserción es cierta: a=1, b=1
En el mundo de la cobertura funcional se considera que una aserción es cubierta si y solo si ha sido habilitada alguna vez. Ni que decir tiene que una aserción sin implicación siempre está habilitada y por tanto siempre es cubierta.