Conception pratique : de la spécification à la majorité à trois entrées

Fixer les conditions avant la réalisation

Construisons un circuit où y=1 si au moins deux entrées parmi a,b,c valent 1. Les entrées sont des 0/1 stables, de même poids, et le circuit ne mémorise pas les anciennes entrées. « Exactement deux » et « au moins deux » diffèrent pour 111.

Chaque terme exprime que deux entrées valent simultanément 1. On peut factoriser en $y=ab+c(a+b)$. Le choix le plus rapide dépend des cellules et des temps d'arrivée.

La majorité est la retenue de l'additionneur complet

Lisez cin comme la troisième entrée c. cout est notre y ; sum est la parité impaire^{iParité Indique si le nombre de bits à 1 est pair ou impair. Le contrôle de parité détecte un nombre impair d'erreurs de bits, mais peut manquer un nombre pair. En savoir plus}. Comparer 001 et 111 révèle l'erreur consistant à utiliser la parité comme majorité.

Construire la référence séparément, depuis la spécification

Copier (a & b) | (a & c) | (b & c) dans le modèle de référence peut reproduire la même erreur. Utilisez une référence entière calculant « au moins deux bits à 1 ».

module voter3(input logic a, b, c, output logic y);
  assign y = (a & b) | (a & c) | (b & c);
endmodule

module tb;
  timeunit 1ns;
  timeprecision 1ps;
  logic a, b, c, y;
  int ones;
  voter3 dut(.*);
  initial begin
    for (int v = 0; v < 8; v++) begin
      {a, b, c} = v[2:0];
      #1;
      ones = int'(a) + int'(b) + int'(c);
      assert (y === (ones >= 2))
        else $fatal(1, "voter mismatch at %03b", {a,b,c});
    end
    $finish;
  end
endmodule

L'extension de chaque bit en int évite les ambiguïtés de largeur de l'arithmétique sur un bit. #1 laisse la logique combinatoire du test se mettre à jour ; cela ne prouve pas qu'une puce réelle fonctionne en 1 ns.

Modifier la spécification et chercher un contre-exemple

Ajouter l'autorisation e donne $y=e(ab+ac+bc)$. Les quatre entrées exigent désormais 16 combinaisons pour un test exhaustif. Vérifiez aussi l'invariant^{iInvariant Condition devant rester vraie dans toute exécution autorisée. Par exemple, l'occupation d'un FIFO de profondeur 4 reste toujours entre 0 et 4. En savoir plus} : si e=0, a,b,c ne doivent plus influencer la sortie.