Esercitazione: dalla specifica alla maggioranza a tre ingressi

Fissare le condizioni prima dell'implementazione

Progettiamo y=1 quando almeno due ingressi fra a, b, c valgono 1. Assumiamo ingressi 0/1 stabili, con lo stesso peso e senza memoria degli ingressi precedenti. «Esattamente due» e «almeno due» differiscono su 111.

Ogni termine indica due ingressi contemporaneamente a 1. La stessa funzione si fattorizza in $y=ab+c(a+b)$. La versione più veloce dipende dalle celle e dai tempi d'arrivo.

La maggioranza coincide con il carry del sommatore completo

Leggete cin come terzo ingresso c. cout è il nostro y, mentre sum è la parità dispari^{iParità Indica se il numero di bit a 1 è pari o dispari. Rileva un numero dispari di errori, ma può non rilevarne un numero pari. Approfondisci}. Confrontando 001 e 111 si riconosce l'errore di usare la parità al posto della maggioranza.

Ricavare il riferimento separatamente dalla specifica

Copiare (a & b) | (a & c) | (b & c) nel modello di riferimento può duplicare lo stesso errore. Usiamo invece un calcolo intero della specifica «almeno due 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'estensione di ogni bit a int evita ambiguità di larghezza nell'aritmetica a un bit. #1 concede al circuito combinatorio simulato il tempo di aggiornarsi; non dimostra che il chip reale operi in 1 ns.

Cambiare la specifica e cercare controesempi

Aggiungendo l'abilitazione e, si ottiene $y=e(ab+ac+bc)$. Ora gli ingressi sono quattro e una verifica esaustiva richiede 16 combinazioni. Verificate anche l'invariante^{iInvariante Condizione sempre vera in ogni esecuzione ammessa. Una FIFO profonda quattro contiene, per esempio, sempre da zero a quattro elementi. Approfondisci} secondo cui con e=0 tutti gli ingressi a, b, c devono essere ignorati.