Dies ist der Befehlsnachweis, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
Beweis – Formaler Beweis zwischen zwei Verhaltensbeschreibungen
ZUSAMMENFASSUNG
Beweis [-a] [-d] file1 file2
BESCHREIBUNG
Entwickelt, um auf einer Datenflussbeschreibung zu laufen, Beweis unterstützt die gleiche Teilmenge von VHDL wie Asimut
und Boom and Boog (weitere Informationen zu dieser Teilmenge erhalten Sie beim VHDL).
Handbuch). Beweis verwendet eine reduzierte geordnete binäre Entscheidungsdiagrammdarstellung, die dies ermöglicht
Der Designer kann die funktionale Äquivalenz zwischen zwei Verhaltensweisen leicht nachweisen
Beschreibungen. Beweis wird im Allgemeinen verwendet, um eine Verhaltensspezifikation zu vergleichen
mit einem extrahierten Verhalten, erhalten durch Yagle.
Im Standardmodus wird eine Reduzierphase für die Beschreibung durchgeführt, indem alle entfernt werden
Hilfssignale (das BDD der Ausgänge, die Register und die Busse) werden ab beschrieben
die Eingänge oder die Register). Die beiden Beschreibungen müssen die gleichen Ressourcen enthalten
(Signale registrieren sich mit demselben Namen). Es ist möglich, die zu verwenden . Inf Datei in Yagle (sehen
weitere Bemerkung zu YAGLE in diesem Dokument), um die Register im extrahierten umzubenennen
Verhaltensbeschreibung (siehe Mann Yagle). Die Daten und die Befehle (die geschützten
Ausdrücke) müssen separat übereinstimmen. Die Busse entsprechen vollständig spezifizierter Logik
Funktionen werden in beiden Beschreibungen durch einen logischen Multiplexer dargestellt. Die Zwei
Beschreibungen müssen die gleiche Schnittstelle (VHDL-Entität) haben, andernfalls die formale Beweis
ist gestoppt.
Beweis Verwendet nur zwei Systemumgebungsvariablen, die sich auf das Arbeitsverzeichnis beziehen.
VARIABLEN
MBK_WORK_LIB gibt den Pfad für die Verhaltensbeschreibungen an. Der Standardwert ist
Aktuelles Verzeichnis.
MBK_CATA_LIB gibt einige Hilfspfade für die Verhaltensbeschreibungen an. Der Standard
value ist das aktuelle Verzeichnis.
OPTIONAL
Optionen können in beliebiger Reihenfolge vor den Dateinamen angegeben werden.
-a Diese Option fragt Beweis um die gemeinsamen Hilfssignale beizubehalten. Beweis behält alles
Zwischensignale, die in beiden Beschreibungen den gleichen Namen haben (ein gemeinsames Signal
wird als Eingabe und Ausgabe jeder Beschreibung betrachtet). Diese Option kann sein
nützlich für Beschreibungen, die große Gleichungen enthalten. Es kann verwendet werden, wenn Beweis hat
fehlgeschlagen ist oder wenn Sie die beiden verschiedenen Beschreibungen im Schritt-für-Schritt-Modus debuggen möchten.
-d Das Programm zeigt Fehler an, wenn die Verhaltensbeschreibungen unterschiedlich sind. Gleichungen
werden angezeigt, wenn es möglich ist.
BEISPIEL
Beweis -a -d Addierer1 Addierer2
YAGLE
YAGLE (Funktionale Abstraktion) wird jetzt kommerziell von Avertec vertrieben
(http://www.avertec.com/). Weitere Informationen erhalten Sie auf deren Website. Binärdateien
Dieses Tool kann auch für nicht-kommerzielle universitäre Forschungszwecke heruntergeladen werden.
Nutzen Sie Beweise online über die Dienste von onworks.net
