Existen varios operadores que nos permiten combinar varias comprobaciones de secuencias . Los efectos son claros si estas secuencias forman parte de la aserción pero no de la habilitación (solo la or es plausible en lacondición de la implicación) y vamos a describirlos
- operador or: si nuestra aserción combina dos secuencias con una or, basta con que una de ellas sea cierta (ocurra) para que se considere que la aserción no falla
- operador and: si nuestra aserción combina dos secuencias con una and, las dos secuencias deben ser ciertas (ocurrir) para que se considere que la aserción no falla
- operador intersect: si nuestra aserción combina dos secuencias con un intersect, las dos secuencias deben ser ciertas (ocurrir) para que se considere que la aserción no falla y además deben finalizar al únísono
- operador within: si nuestra aserción combina dos secuencias con within, las dos secuencias deben ser ciertas (ocurrir) y además una de ellas debe contener completamente a la otra
Ejemplos
Ejemplo1
|
1 |
assert property (@(posedge clk) a ##1 !a ##1 a |-> (##1 g ##1 !g) or (##1 !g[*2]) |
| g: | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | |
| a: | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 1 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
Puede observarse que la aserción no falla nunca porque las dos veces que la habilitación es cierta (ciclos 3 y 5) o bien ha ocurrido una secuencia o la otra de las combinadas mediante la expresión or
Ejemplo2
|
1 |
assert property (@(posedge clk) rose(r) |=> (!g[*2:$] ##1 g ) and (r [*2:$] ##1 !r) |
| g: | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | |
| r: | 0 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
Podemos observar que esta aserción tampoco falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que había que comprobar en la aserción ocurrieron. Cierto es que dichas secuencias terminaron de ser ciertas en momentos diferentes; pero eso no es chequeado por la expresión and
Ejemplo 3
|
1 |
assert property (@(posedge clk) rose(r) |=> (!g[*2:$] ##1 g ) intersect (r [*2:$] ##1 !r) |
| g: | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | |
| r: | 0 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
Podemos observar que esta aserción si que falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que había que comprobar en la aserción ocurrieron; pero terminaron de ser ciertas en momentos diferentes. En el ciclo 4 ya observa la aserción que las dos secuencias no han sido ciertas al mismo tiempo y da fallo
Ejemplo 4
|
1 |
assert property (@(posedge clk) rose(r) |=> (!g[*2:$] ##1 g ) within (r [*2:$] ##1 !r) |
| g: | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | |
| r: | 0 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | |
| c: | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
Podemos observar que esta aserción no falla porque cuando fue habilitada (ciclo 1) , ambas secuencias que había que comprobar en la aserción ocurrieron; y la secuencia segunda (en verde) contiene completamente a la primera (en azul)