moka – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

MOKA – Vorfahr des Modellprüfers

ZUSAMMENFASSUNG

Mokka [-VDB] fsm_filename ctl_filename

BESCHREIBUNG

Mokka ist ein CTL-Modellprüfer.

Entwickelt, um auf FSM- oder RTL-Beschreibungen zu laufen, Mokka unterstützt die gleiche VHDL-Teilmenge wie syf oder boom
(Weitere Informationen zu dieser Teilmenge finden Sie unter SYF(1) BOOM(1) FSM(5) VBE(5)).
dennoch Mokka setzt voraus, dass jedes Register der Verhaltensbeschreibung dasselbe hat
Taktzustand und dass keine Tristate- oder Multiplex-Busse vorhanden sind. Insbesondere VHDL
Typ MUX_BIT und WOR_BIT werden nicht unterstützt.
Zunächst Mokka Erstellen Sie den Funktionsübergang des FSM mithilfe einer reduzierten geordneten Binärdatei
Darstellung von Entscheidungsdiagrammen.
Anschließend wendet es die Anfangsbedingungen an, um den ersten Zustand zu finden (Schlüsselwort INITIAL und/oder
RESET_COND im CTL(5) Dateiformat).
Anschließend wird eine symbolische Simulation des FSM berechnet, um alle erreichbaren Zustände zu finden.
Bei dieser Berechnung werden die Annahmebedingungen berücksichtigt (Schlüsselwort ASSUME im
CTL(5) Dateiformat).
Mokka Verifiziert schließlich jede CTL-Formel einzeln. (sehen CTL(5) für das CTL-Dateiformat
Einzelheiten).

CTL BETREIBER

Für jeden CTL-Unterausdruck Mokka gibt die Menge der Zustände zurück, die die Formel verifiziert.
Beispielsweise gibt EX(p) den Satz erreichbarer Zustände zurück, der EX(p) verifiziert.
CTL-Operatoren:
EX(p) : Gibt alle Zustände zurück, die fast einen primären Nachfolger haben
überprüft p.
EU(p,q) : Gibt alle Zustände zurück, die die Wurzel fast eines Pfades sind, also p is
wahr bis q ist immer wahr.
EG(p) : gibt alle Zustände zurück, die die Wurzel fast eines Pfades sind, so dass p is
immer wahr.
AX(p) : gibt alle Staaten zurück, die alle ihre primären Nachfolger haben
überprüft p.
AU(p,q) : gibt alle Zustände zurück, die die Wurzel von nur Pfaden sind, von denen p ist wahr
bis q ist immer wahr.
AG(p) : gibt alle Zustände zurück, die nur die Wurzel von Pfaden sind, so dass p immer
wahr.

VARIABLEN

MBK_WORK_LIB gibt den Pfad für die Beschreibung und die CTL-Datei an. Der Standardwert ist
das aktuelle Verzeichnis.

MBK_CATA_LIB Gibt einige Hilfspfade für die Beschreibungen und die CTL-Datei an. Der
Der Standardwert ist das aktuelle Verzeichnis.

OPTIONAL

-V Aktiviert den ausführlichen Modus. Jeder Schritt der Modellprüfung wird im Standard angezeigt
Ausgabe.

-D Aktiviert den Debug-Modus. Jeder Schritt der Modellprüfung wird in der Standardausgabe detailliert beschrieben.
Insbesondere werden für jeden CTL-Unterausdruck alle gesetzten Zustände angezeigt.

-B Die Eingabedatei ist eine VHDL-Beschreibung unter Verwendung der Alliance-VHDL-Teilmenge (siehe VBE(5) Datei
Format).

FSM BEISPIEL

-- Ein Multi-FSM-Beispiel

ENTITY-Beispiel ist
PORT
(
ck: in BIT;
data_in: in BIT;
zurücksetzen: in BIT;
data_out: out BIT
);
END-Beispiel;

ARCHITEKTUR FSM Beispiel ist

TYP A_ETAT_TYPE IS (A_E0, A_E1);
SIGNAL A_NS, A_CS : A_ETAT_TYPE;

TYP B_ETAT_TYPE IS (B_E0, B_E1);
SIGNAL B_NS, B_CS : B_ETAT_TYPE;

--PRAGMA CURRENT_STATE A_CS FSM_A
--PRAGMA NEXT_STATE A_NS FSM_A
--PRAGMA CLOCK ck FSM_A
--PRAGMA FIRST_STATE A_E0 FSM_A

--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--PRAGMA CLOCK ck FSM_B
--PRAGMA FIRST_STATE B_E0 FSM_B

SIGNAL ACK, REQ, DATA_INT : BIT;

START

A_1: PROZESS (A_CS, ACK)
START
WENN (zurücksetzen = '1')
DANN A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ELSE
CASE A_CS ist
WANN A_E0 =>
IF ( ACK ='1') THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
ENDE WENN;
DATA_OUT <= '0';
REQ <= '1';
WANN A_E1 =>
IF ( ACK ='1') THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
ENDE WENN;
DATA_OUT <= DATA_INT;
REQ <= '0';
ENDGEHÄUSE;
ENDE WENN;
ENDE PROZESS A_1;

A_2: PROZESS(ck)
START
IF (ck = '1' UND NICHT ck'STABLE)
DANN A_CS <= A_NS;
ENDE WENN;
ENDE PROZESS A_2;

-------

B_1: PROZESS (B_CS, ACK)
START
WENN (zurücksetzen = '1')
DANN B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
ELSE
CASE B_CS ist
WHEN B_E0 =>
IF ( REQ ='1') THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
ENDE WENN;
DATA_INT <= '0';
ACK <= '0';
WHEN B_E1 =>
IF ( REQ ='1') THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
ENDE WENN;
DATA_INT <= DATA_IN;
ACK <= '1';
ENDGEHÄUSE;
ENDE WENN;
ENDE PROZESS B_1;

B_2: PROZESS(ck)
START
IF (ck = '1' UND NICHT ck'STABLE)
DANN B_CS <= B_NS;
ENDE WENN;
ENDE PROZESS B_2;

ENDE FSM;

CTL BEISPIEL

– Ein Beispiel für eine CTL-Datei

TYP A_ETAT_TYPE IS (A_E0, A_E1);
TYP B_ETAT_TYPE IS (B_E0, B_E1);

VARIABLE A_NS, A_CS : A_ETAT_TYPE;
VARIABLE B_NS, B_CS : B_ETAT_TYPE;

VARIABLE ck: BIT;
VARIABLE data_in : BIT;
VARIABLE data_out : BIT;
VARIABLEN-Reset: BIT;
VARIABLE ack: BIT;
VARIABLE erforderlich: BIT;

RESET_COND init1 := (reset='1');
ASSUME ass1 := (reset='0');

beginnen

prop1 : EX( ack='1' );
prop2: AG(req -> AF(ack));
prop4: AU( req='1', ack='1');

end;

MOKA BEISPIEL

moka -V Beispielbeispiel

Nutzen Sie Moka online über die Dienste von onworks.net