Assertions immédiates et SVA

Contrôler une condition locale, exprimer une règle sur plusieurs cycles et désactiver proprement les propriétés pendant le reset.

Une assertion pour une règle précise

Une assertion signale qu'une condition supposée vraie ne l'est pas. Elle ne remplace pas le scoreboard : elle contrôle surtout des invariants, des règles de protocole et des relations temporelles locales.

Une assertion immédiate est évaluée au moment où le programme l'exécute.

always_comb begin
  assert (!$isunknown({i_valid, i_ready}))
    else $error("Handshake contains X or Z");
end

Elle convient à une condition combinatoire ou à un contrôle dans une tâche. Elle ne garde pas d'historique sur plusieurs cycles.

Une propriété temporelle

SVA permet d'exprimer une relation entre événements échantillonnés sur une horloge.

property request_gets_response;
  @(posedge i_clk) disable iff (i_rst)
    i_request |-> ##[1:4] o_response;
endproperty
 
assert property (request_gets_response)
  else $error("No response within four cycles");

|-> est une implication chevauchante. Si i_request est vrai au cycle de départ, la conséquence commence sur ce même cycle. Le délai ##[1:4] demande ensuite o_response entre un et quatre cycles plus tard.

Avec |=>, la conséquence commence au cycle suivant. Le choix doit correspondre exactement au protocole.

Stabilité sous contre-pression

Un protocole valid/ready demande souvent que les données restent stables tant que valid vaut 1 et que ready vaut 0.

property hold_data_while_stalled;
  @(posedge i_clk) disable iff (i_rst)
    i_valid && !i_ready |=> i_valid && $stable(i_data);
endproperty
 
assert property (hold_data_while_stalled);

Cette propriété vérifie le cycle qui suit chaque cycle bloqué. Selon la définition du protocole, il peut aussi être nécessaire d'inclure d'autres champs comme last, l'adresse ou les octets valides.

Reset et inconnues

disable iff (i_rst) abandonne les tentatives en cours et désactive la propriété pendant le reset. La polarité et le caractère synchrone ou asynchrone doivent correspondre au design.

Une assertion peut passer de façon trompeuse si son antécédent n'arrive jamais. Une propriété de couverture complémentaire montre qu'un scénario a bien été observé :

cover property (@(posedge i_clk) disable iff (i_rst)
  i_request ##[1:4] o_response);

Rester lisible

Une propriété courte avec un nom clair est plus facile à maintenir qu'une expression unique de plusieurs lignes. Écrire d'abord la règle en français simple, définir le cycle de départ et dessiner deux ou trois chronogrammes avant de coder la propriété.

À retenir

• Une assertion immédiate contrôle une condition au point d'exécution.
• Une assertion concurrente échantillonne une relation dans le temps.
• |-> et |=> ne démarrent pas la conséquence au même cycle.
• disable iff gère les tentatives pendant le reset.
• Une propriété peut passer sans être exercée, d'où l'intérêt de la couverture.

📝 Tester mes connaissances - Quiz du chapitre