മോക്ക - ക്ലൗഡിൽ ഓൺലൈനിൽ

പട്ടിക:

NAME

മോക്ക - മോഡൽ ചെക്കർ പൂർവ്വികൻ

സിനോപ്സിസ്

മോക [-VDB] fsm_ഫയലിന്റെ പേര് ctl_ഫയലിന്റെ പേര്

വിവരണം

മോക ഒരു CTL മോഡൽ ചെക്കറാണ്.

FSM അല്ലെങ്കിൽ RTL വിവരണങ്ങളിൽ പ്രവർത്തിപ്പിക്കുന്നതിനായി നിർമ്മിച്ചത്, മോക syf അല്ലെങ്കിൽ boom പോലെയുള്ള VHDL ഉപസെറ്റിനെ പിന്തുണയ്ക്കുന്നു
(ഈ ഉപവിഭാഗത്തെക്കുറിച്ചുള്ള കൂടുതൽ വിവരങ്ങൾക്ക് കാണുക SYF(1), BOOM(1), രാജ്യം(5), വി.ബി.ഇ(5) ).
എന്നിരുന്നാലും മോക പെരുമാറ്റ വിവരണത്തിന്റെ ഓരോ രജിസ്റ്ററിനും ഒന്നുതന്നെയുണ്ടെന്ന് ചുമത്തുന്നു
ട്രൈസ്‌റ്റേറ്റ് അല്ലെങ്കിൽ മൾട്ടിപ്ലക്‌സ് ബസുകൾ ഇല്ല എന്നതും ക്ലോക്ക് അവസ്ഥയും. പ്രത്യേകിച്ച് വി.എച്ച്.ഡി.എൽ
തരം MUX_BIT, WOR_BIT എന്നിവ പിന്തുണയ്ക്കുന്നില്ല.
ഒന്നാമതായി മോക ഒരു റിഡ്യൂസ്ഡ് ഓർഡർഡ് ബൈനറി ഉപയോഗിച്ച് FSM-ന്റെ ഫംഗ്ഷൻ ട്രാൻസിഷൻ നിർമ്മിക്കുക
തീരുമാന രേഖാചിത്രങ്ങളുടെ പ്രാതിനിധ്യം.
ആദ്യ അവസ്ഥ കണ്ടെത്തുന്നതിന് ഇത് പ്രാരംഭ വ്യവസ്ഥകൾ പ്രയോഗിക്കുന്നു (കീവേഡ് INITIAL കൂടാതെ/അല്ലെങ്കിൽ
ഇതിൽ RESET_COND സി.ടി.എൽ.(5) ഫയൽ ഫോർമാറ്റ്).
എത്തിച്ചേരാവുന്ന എല്ലാ അവസ്ഥകളും കണ്ടെത്തുന്നതിന് FSM-ന്റെ പ്രതീകാത്മക സിമുലേഷൻ കണക്കാക്കിയ ശേഷം.
ഈ കണക്കുകൂട്ടൽ അനുമാന വ്യവസ്ഥകൾ (ASSUME കീവേഡ് ഇൻ
സി.ടി.എൽ.(5) ഫയൽ ഫോർമാറ്റ്).
മോക ഒടുവിൽ ഓരോ CTL ഫോർമുലകളും ഓരോന്നായി പരിശോധിക്കുന്നു. (കാണുക സി.ടി.എൽ.(5) CTL ഫയൽ ഫോർമാറ്റിനായി
വിശദാംശങ്ങൾ).

സി.ടി.എൽ. ഓപ്പറേറ്റർമാർ

ഓരോ CTL ഉപ-പ്രകടനത്തിനും മോക ഫോർമുല സ്ഥിരീകരിക്കുന്ന സംസ്ഥാനങ്ങളുടെ കൂട്ടം തിരികെ നൽകും.
ഉദാഹരണത്തിന്, EX(p) എന്നത് EX(p) പരിശോധിച്ചുറപ്പിക്കുന്ന എത്തിച്ചേരാവുന്ന അവസ്ഥകളുടെ സെറ്റ് തിരികെ നൽകും.
CTL ഓപ്പറേറ്റർമാർ:
EX(p) : ഏതാണ്ട് ഒരു പ്രാഥമിക സംസ്ഥാന പിൻഗാമിയുള്ള എല്ലാ സംസ്ഥാനങ്ങളും നൽകുന്നു
പരിശോധിച്ചുറപ്പിക്കുന്നു p.
EU(p,q): ഏതാണ്ട് ഒരു പാതയുടെ മൂലമായ എല്ലാ സംസ്ഥാനങ്ങളും തിരികെ നൽകുന്നു p is
വരെ സത്യമാണ് q എപ്പോഴും സത്യമാണ്.
EG(p) : ഏതാണ്ട് ഒരു പാതയുടെ മൂലമായ എല്ലാ അവസ്ഥകളും നൽകുന്നു p is
എപ്പോഴും സത്യം.
AX(p) : എല്ലാ പ്രാഥമിക സംസ്ഥാന പിൻഗാമികളും ഉള്ള എല്ലാ സംസ്ഥാനങ്ങളും നൽകുന്നു
പരിശോധിച്ചുറപ്പിക്കുന്നു p.
AU(p,q): പാതകളുടെ മാത്രം മൂലമായ എല്ലാ അവസ്ഥകളും നൽകുന്നു p സത്യമാണ്
വരുവോളം q എപ്പോഴും സത്യമാണ്.
AG(p) : പാതകളുടെ മാത്രം മൂലമായ എല്ലാ അവസ്ഥകളും നൽകുന്നു p എപ്പോഴും
ശരി.

ENVIRONMENT വ്യത്യാസങ്ങൾ

Mbk_work_lib വിവരണത്തിനും CTL ഫയലിനുമുള്ള പാത നൽകുന്നു. സ്ഥിര മൂല്യം ആണ്
നിലവിലെ ഡയറക്‌ടറി.

MBK_CATA_LIB വിവരണങ്ങൾക്കും CTL ഫയലിനും ചില സഹായ പാതകൾ നൽകുന്നു. ദി
നിലവിലെ ഡയറക്‌ടറിയാണ് സ്ഥിര മൂല്യം.

ഓപ്ഷനുകൾ

-വി വെർബോസ് മോഡ് ഓണാക്കുന്നു. മോഡൽ പരിശോധനയുടെ ഓരോ ഘട്ടവും സ്റ്റാൻഡേർഡിൽ പ്രദർശിപ്പിക്കും
.ട്ട്‌പുട്ട്.

-D ഡീബഗ് മോഡ് ഓണാക്കുന്നു. മാതൃകാ പരിശോധനയുടെ ഓരോ ഘട്ടവും സ്റ്റാൻഡേർഡ് ഔട്ട്പുട്ടിൽ വിശദമായി പ്രതിപാദിച്ചിരിക്കുന്നു.
പ്രത്യേകിച്ചും ഓരോ CTL ഉപ-എക്‌സ്‌പ്രഷനും എല്ലാ സ്‌റ്റേറ്റുകളും പ്രദർശിപ്പിച്ചിരിക്കുന്നു.

-B അലയൻസ് VHDL ഉപസെറ്റ് ഉപയോഗിക്കുന്ന ഒരു VHDL വിവരണമാണ് ഇൻപുട്ട് ഫയൽ (കാണുക വി.ബി.ഇ(5) ഫയൽ
ഫോർമാറ്റ്).

രാജ്യം ഉദാഹരണം

-- ഒരു മൾട്ടി എഫ്എസ്എം ഉദാഹരണം

ENTITY ഉദാഹരണമാണ്
പോർട്ട്
(
ck : BIT ൽ;
data_in : BIT-ൽ;
പുനഃസജ്ജമാക്കുക : BIT ൽ;
ഡാറ്റ_ഔട്ട്: ഔട്ട് ബിറ്റ്
);
END ഉദാഹരണം;

ആർക്കിടെക്ചർ എഫ്എസ്എം ഉദാഹരണമാണ്

TYPE A_ETAT_TYPE IS (A_E0, A_E1);
സിഗ്നൽ A_NS, A_CS : A_ETAT_TYPE;

TYPE B_ETAT_TYPE IS (B_E0, B_E1);
സിഗ്നൽ 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

സിഗ്നൽ ACK, REQ, DATA_INT : BIT;

ആരംഭിക്കുന്നു

A_1 : പ്രോസസ്സ് ( A_CS, ACK )
ആരംഭിക്കുന്നു
IF (റീസെറ്റ് = '1' )
അപ്പോൾ A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
വേറെ
CASE A_CS ആണ്
എപ്പോൾ A_E0 =>
എങ്കിൽ (ACK ='1') പിന്നെ A_NS <= A_E1;
ELSE A_NS <= A_E0;
എങ്കിൽ അവസാനിപ്പിക്കുക;
DATA_OUT <= '0';
REQ <= '1';
എപ്പോൾ A_E1 =>
എങ്കിൽ (ACK ='1') പിന്നെ A_NS <= A_E1;
ELSE A_NS <= A_E0;
എങ്കിൽ അവസാനിപ്പിക്കുക;
DATA_OUT <= DATA_INT;
REQ <= '0';
END കേസ്;
എങ്കിൽ അവസാനിപ്പിക്കുക;
പ്രക്രിയ അവസാനിപ്പിക്കുക A_1;

A_2 : PROCESS( ck )
ആരംഭിക്കുന്നു
എങ്കിൽ ( ck = '1' ഒപ്പം ck'സ്റ്റേബിൾ അല്ല )
തുടർന്ന് A_CS <= A_NS;
എങ്കിൽ അവസാനിപ്പിക്കുക;
പ്രക്രിയ അവസാനിപ്പിക്കുക A_2;

-------

B_1 : പ്രോസസ്സ് ( B_CS, ACK )
ആരംഭിക്കുന്നു
IF (റീസെറ്റ് = '1' )
തുടർന്ന് B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
വേറെ
CASE B_CS ആണ്
എപ്പോൾ B_E0 =>
എങ്കിൽ (REQ ='1') പിന്നെ B_NS <= B_E1;
ELSE B_NS <= B_E0;
എങ്കിൽ അവസാനിപ്പിക്കുക;
DATA_INT <= '0';
ACK <= '0';
എപ്പോൾ B_E1 =>
എങ്കിൽ (REQ ='1') പിന്നെ B_NS <= B_E1;
ELSE B_NS <= B_E0;
എങ്കിൽ അവസാനിപ്പിക്കുക;
DATA_INT <= DATA_IN;
ACK <= '1';
END കേസ്;
എങ്കിൽ അവസാനിപ്പിക്കുക;
പ്രക്രിയ അവസാനിപ്പിക്കുക B_1;

B_2 : PROCESS( ck )
ആരംഭിക്കുന്നു
എങ്കിൽ ( ck = '1' ഒപ്പം ck'സ്റ്റേബിൾ അല്ല )
തുടർന്ന് B_CS <= B_NS;
എങ്കിൽ അവസാനിപ്പിക്കുക;
പ്രക്രിയ അവസാനിപ്പിക്കുക B_2;

എഫ്എസ്എം അവസാനിപ്പിക്കുക;

സി.ടി.എൽ. ഉദാഹരണം

-- ഒരു CTL ഫയൽ ഉദാഹരണം

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

വേരിയബിൾ A_NS, A_CS : A_ETAT_TYPE;
വേരിയബിൾ B_NS, B_CS : B_ETAT_TYPE;

VARIABLE ck : BIT;
VARIABLE data_in : BIT;
VARIABLE data_out : BIT;
വേരിയബിൾ റീസെറ്റ് : ബിറ്റ്;
വേരിയബിൾ ആക്ക് : ബിറ്റ്;
VARIABLE req : BIT;

RESET_COND init1 := (റീസെറ്റ്='1');
assUME ass1 := (റീസെറ്റ്='0');

ആരംഭിക്കുന്നു

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

അവസാനം;

മോച്ച ഉദാഹരണം

moka -V ഉദാഹരണം

onworks.net സേവനങ്ങൾ ഉപയോഗിച്ച് മോക്ക ഓൺലൈനായി ഉപയോഗിക്കുക