moka - En ligne dans le Cloud

PROGRAMME:

Nom

MOKA - Ancêtre du model checker

SYNOPSIS

moka [-VDB] nom_fichier fsm nom_fichier ctl

DESCRIPTION

moka est un vérificateur de modèles CTL.

Conçu pour fonctionner sur des descriptions FSM ou RTL, moka prend en charge le même sous-ensemble VHDL que syf ou boom
(pour plus d'informations sur ce sous-ensemble voir SYF(1), BOOM(1), FSM(5), VBE(5) ).
Néanmoins moka impose que chaque registre de la description comportementale ait le même
condition d'horloge et qu'il n'y a pas de bus à trois états ou multiplexés. En particulier VHDL
les types MUX_BIT et WOR_BIT ne sont pas pris en charge.
Tout d'abord moka construire la transition de fonction du FSM en utilisant un binaire ordonné réduit
Représentation des diagrammes de décision.
Il applique ensuite les conditions initiales pour trouver le premier état (mot clé INITIAL et/ou
RESET_COND dans le CTL(5) format de fichier).
Ensuite, il calcule une simulation symbolique du FSM afin de trouver tous les états accessibles.
Ce calcul prend en compte les conditions d'hypothèses (mot clé ASSUME dans le
CTL(5) format de fichier).
moka vérifie enfin une à une chaque formule CTL. (voir CTL(5) pour le format de fichier CTL
des détails).

CTL LES OPÉRATEURS

Pour chaque sous-expression CTL moka renverra l'ensemble d'états qui vérifie la formule.
Par exemple, EX(p) renverra l'ensemble d'états atteignables qui vérifie EX(p).
Opérateurs CTL :
EX(p) : renvoie tous les états qui ont presque un premier état successeur qui
vérifie p.
EU(p,q) : renvoie tous les états qui sont la racine de presque un chemin, tels que p is
vrai jusqu'à q est toujours vrai.
EG(p) : renvoie tous les états qui sont la racine de presque un chemin, tels que p is
toujours vrai.
AX(p) : renvoie tous les états qui ont tous leur successeur d'état primaire qui
vérifie p.
AU(p,q) : renvoie tous les états qui sont la racine des seuls chemins à partir desquels p est vrai
jusqu'à q est toujours vrai.
AG(p) : renvoie tous les états qui sont la racine des seuls chemins, tels que p est toujours
vrai.

ENVIRONNEMENT VARIABLES

MBK_WORK_LIB donne le chemin de la description et du fichier CTL. La valeur par défaut est
le répertoire courant.

MBK_CATA_LIB donne quelques chemins auxiliaires pour les descriptions et le fichier CTL. Les
la valeur par défaut est le répertoire courant.

OPTIONS

-V Active le mode détaillé. Chaque étape de la vérification du modèle est affichée sur le standard
sortie.

-D Active le mode de débogage. Chaque étape de la vérification du modèle est détaillée sur la sortie standard.
En particulier, tous les états définis sont affichés pour chaque sous-expression CTL.

-B Le fichier d'entrée est une description VHDL utilisant le sous-ensemble Alliance VHDL (voir VBE(5) fichier
format).

FSM EXEMPLE

-- Un exemple multifsm

L'exemple ENTITY est
PORT
(
ck : en BIT ;
data_in : en BIT;
reset : en BIT ;
data_out : out BIT
);
Exemple de FIN ;

ARCHITECTURE FSM d'exemple est

TYPE A_ETAT_TYPE EST (A_E0, A_E1) ;
SIGNAL A_NS, A_CS : A_ETAT_TYPE ;

TYPE B_ETAT_TYPE EST (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 HORLOGE ck FSM_A
--PRAGMA PREMIER_ÉTAT A_E0 FSM_A

--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--PRAGMA HORLOGE ck FSM_B
--PRAGMA PREMIER_ÉTAT B_E0 FSM_B

SIGNAL ACK, REQ, DATA_INT : BIT ;

COMMENCER

A_1 : PROCESSUS (A_CS, ACK)
COMMENCER
SI ( réinitialiser = '1' )
ALORS A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0' ;
AUTRE
Le CAS A_CS est
QUAND A_E0 =>
SI ( ACK ='1') ALORS A_NS <= A_E1;
SINON A_NS <= A_E0;
END IF;
DATA_OUT <= '0';
REQ <= '1' ;
QUAND A_E1 =>
SI ( ACK ='1') ALORS A_NS <= A_E1;
SINON A_NS <= A_E0;
END IF;
DATA_OUT <= DATA_INT;
REQ <= '0' ;
FIN DE CAS;
END IF;
TERMINER LE PROCESSUS A_1 ;

A_2 : PROCESSUS( ck )
COMMENCER
SI ( ck = '1' ET NON ck'STABLE )
ALORS A_CS <= A_NS ;
END IF;
TERMINER LE PROCESSUS A_2 ;

-------

B_1 : PROCESSUS ( B_CS, ACK )
COMMENCER
SI ( réinitialiser = '1' )
ALORS B_NS <= B_E0 ;
DATA_INT <= '0';
ACK <= '0';
AUTRE
Le CAS B_CS est
QUAND B_E0 =>
SI ( REQ ='1') ALORS B_NS <= B_E1;
SINON B_NS <= B_E0;
END IF;
DATA_INT <= '0';
ACK <= '0';
QUAND B_E1 =>
SI ( REQ ='1') ALORS B_NS <= B_E1;
SINON B_NS <= B_E0;
END IF;
DATA_INT <= DATA_IN;
ACK <= '1';
FIN DE CAS;
END IF;
TERMINER LE PROCESSUS B_1 ;

B_2 : PROCESSUS( ck )
COMMENCER
SI ( ck = '1' ET NON ck'STABLE )
ALORS B_CS <= B_NS ;
END IF;
TERMINER LE PROCESSUS B_2 ;

FIN FSM ;

CTL EXEMPLE

-- Un exemple de fichier CTL

TYPE A_ETAT_TYPE EST (A_E0, A_E1) ;
TYPE B_ETAT_TYPE EST (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 ;
Réinitialisation VARIABLE : BIT ;
VARIABLE ACK : BIT ;
VARIABLE demande : BIT ;

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

commencer

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

fin;

MOKA EXEMPLE

moka -V exemple exemple

Utilisez moka en ligne en utilisant les services onworks.net