Entwurfsübung: Von der Spezifikation zur Dreieingangsmehrheit

Bedingungen vor der Implementierung festlegen

Wir entwerfen eine Schaltung mit y=1, wenn von a, b, c mindestens zwei Eingänge 1 sind. Die Eingänge seien stabile 0/1-Werte, gleich gewichtet und ohne Speicherung früherer Eingaben. „Genau zwei“ und „mindestens zwei“ unterscheiden sich bei 111.

Jeder Term steht für zwei gleichzeitig gesetzte Eingänge. Dieselbe Funktion lässt sich zu $y=ab+c(a+b)$ faktorisieren. Welche Form schneller ist, hängt von Zellen und Ankunftszeiten ab.

Mehrheit entspricht dem Übertrag eines Volladdierers

Lesen Sie cin unten als dritten Eingang c. cout ist unser y, sum die ungerade Parität^{iParität Gibt an, ob die Anzahl gesetzter Bits gerade oder ungerade ist. Paritätsprüfung erkennt ungerade viele Bitfehler, kann gerade viele jedoch übersehen. Mehr erfahren}. Der Vergleich von 001 und 111 zeigt, warum es falsch ist, Parität als Mehrheitsfunktion zu verwenden.

Den Prüfmaßstab unabhängig aus der Spezifikation bilden

Wird (a & b) | (a & c) | (b & c) unverändert als Referenzmodell kopiert, kann derselbe Fehler in beiden stehen. Berechnen Sie stattdessen die Spezifikation „mindestens zwei Einsen“ mit Ganzzahlen.

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

Die Erweiterung jedes Bits zu int vermeidet Breitenverwechslungen in 1-Bit-Arithmetik. #1 gibt der kombinatorischen Simulation Zeit zum Aktualisieren und beweist keinen Betrieb des realen Chips in 1 ns.

Die Spezifikation ändern und Gegenbeispiele finden

Mit einer Ausgangsfreigabe e gilt $y=e(ab+ac+bc)$. Vier Eingänge verlangen jetzt 16 Kombinationen für eine vollständige Prüfung. Prüfen Sie zusätzlich die Invariante^{iInvariante Bedingung, die bei jeder zulässigen Ausführung stets wahr bleiben muss. Eine FIFO mit Tiefe vier enthält etwa immer zwischen null und vier Elemente. Mehr erfahren}, dass bei e=0 alle a, b, c ignoriert werden.