मोका - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

मोका - मॉडल चेकर पूर्वज

SYNOPSIS

मोका [-वीडीबी] fsm_filename ctl_filename

वर्णन

मोका एक सीटीएल मॉडल चेकर है।

FSM या RTL विवरण पर चलने के लिए बनाया गया, मोका syf या बूम के समान VHDL उपसमुच्चय का समर्थन करता है
(इस उपसमुच्चय के बारे में अधिक जानकारी के लिए देखें SYF(1) बूम(1) FSM(5) VBE(5) )।
फिर भी मोका लागू करता है कि व्यवहार विवरण के प्रत्येक रजिस्टर में समान है
घड़ी की स्थिति और यह कि कोई ट्रिस्टेट या मल्टीप्लेक्स बसें नहीं हैं। विशेष रूप से वीएचडीएल
MUX_BIT टाइप करें और WOR_BIT समर्थित नहीं हैं।
सब से पहले मोका एक कम आदेशित बाइनरी का उपयोग करके एफएसएम के फॉनक्शन ट्रांजिशन का निर्माण करें
निर्णय आरेख प्रतिनिधित्व।
इसके बाद यह पहली स्थिति खोजने के लिए प्रारंभिक शर्तें लागू करता है (कीवर्ड INITIAL और/या
में RESET_COND सीटीएल(5) फ़ाइल प्रारूप)।
इसके बाद सभी पहुंच योग्य राज्यों को खोजने के लिए एफएसएम के प्रतीकात्मक अनुकरण की गणना करता है।
यह गणना मान्यताओं की स्थिति (ASSUME कीवर्ड में) को ध्यान में रखती है
सीटीएल(5) फ़ाइल प्रारूप)।
मोका अंत में प्रत्येक सीटीएल सूत्रों को एक-एक करके सत्यापित करता है। (देख सीटीएल(5) सीटीएल फ़ाइल प्रारूप के लिए
विवरण)।

सीटीएल ऑपरेटरों

प्रत्येक सीटीएल उप-अभिव्यक्ति के लिए मोका सूत्र की पुष्टि करने वाले राज्यों का समूह लौटाएगा।
उदाहरण के लिए EX(p) पहुंच योग्य अवस्थाओं का सेट लौटाएगा जो EX(p) की पुष्टि करता है।
सीटीएल ऑपरेटर:
EX(p) : उन सभी राज्यों को लौटाता है जिनके पास लगभग एक प्राथमिक राज्य उत्तराधिकारी है
लेखा परीक्षित p.
EU(p,q): सभी राज्यों को लौटाता है जो लगभग एक पथ की जड़ हैं, जैसे कि p is
सच जब तक q हमेशा सच होता है।
ईजी (पी): सभी राज्यों को लौटाता है जो लगभग एक पथ की जड़ हैं, जैसे कि p is
अटल सत्य।
AX(p) : उन सभी राज्यों को लौटाता है जिनके सभी प्राथमिक राज्य उत्तराधिकारी हैं
लेखा परीक्षित p.
AU(p,q): उन सभी राज्यों को लौटाता है जो केवल पथों के मूल हैं, जिनसे p सच हैं
जब तक q हमेशा सच होता है।
AG(p): सभी राज्यों को लौटाता है जो केवल पथों की जड़ हैं, जैसे कि p हमेशा है
सच है।

वातावरण चर

एमबीके_WORK_LIB विवरण और सीटीएल फ़ाइल के लिए पथ देता है। डिफ़ॉल्ट मान है
वर्तमान निर्देशिका।

एमबीके_CATA_LIB विवरण और सीटीएल फ़ाइल के लिए कुछ सहायक पथ देता है। NS
डिफ़ॉल्ट मान वर्तमान निर्देशिका है।

विकल्प

-V वर्बोज़ मोड को चालू करता है। मॉडल जाँच का प्रत्येक चरण मानक पर प्रदर्शित होता है
उत्पादन.

-D डिबग मोड को चालू करता है। मॉडल जाँच का प्रत्येक चरण मानक आउटपुट पर विस्तृत है।
विशेष रूप से सभी राज्यों के सेट प्रत्येक सीटीएल उप-अभिव्यक्ति के लिए प्रदर्शित होते हैं।

-बी इनपुट फ़ाइल एलायंस वीएचडीएल सबसेट का उपयोग करते हुए एक वीएचडीएल विवरण है (देखें VBE(5) फ़ाइल
प्रारूप).

FSM उदाहरण

-- एक बहु fsm उदाहरण

ENTITY उदाहरण है
पोर्ट
(
सीके: बीआईटी में;
data_in : बीआईटी में;
रीसेट : बीआईटी में;
data_out : बाहर बिट
);
अंत उदाहरण;

उदाहरण के वास्तुकला एफएसएम है

प्रकार A_ETAT_TYPE है (A_E0, A_E1);
सिग्नल A_NS, A_CS: A_ETAT_TYPE;

प्रकार B_ETAT_TYPE है (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
--प्रगमा घड़ी सीके FSM_A
--PRAGMA FIRST_STATE A_E0 FSM_A

--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--प्रगमा घड़ी सीके FSM_B
--PRAGMA FIRST_STATE B_E0 FSM_B

सिग्नल एसीके, आरईक्यू, डेटा_आईएनटी: बिट;

शुरू

ए_1: प्रक्रिया (ए_सीएस, एसीके)
शुरू
अगर (रीसेट = '1')
तब A_NS <= A_E0;
डेटा_आउट <= '0';
आरईक्यू <= '0';
और
मामला A_CS है
जब A_E0 =>
अगर (एसीके ='1') तब A_NS <= A_E1;
ELSE A_NS <= A_E0;
अगर अंत;
डेटा_आउट <= '0';
आरईक्यू <= '1';
जब A_E1 =>
अगर (एसीके ='1') तब A_NS <= A_E1;
ELSE A_NS <= A_E0;
अगर अंत;
DATA_OUT <= DATA_INT;
आरईक्यू <= '0';
अंत मामला;
अगर अंत;
प्रक्रिया समाप्त करें A_1;

ए_2: प्रक्रिया (सीके)
शुरू
अगर (सीके = '1' और सीके 'स्थिर नहीं)
तब A_CS <= A_NS;
अगर अंत;
प्रक्रिया समाप्त करें A_2;

-------

बी_1: प्रक्रिया (बी_सीएस, एसीके)
शुरू
अगर (रीसेट = '1')
तब B_NS <= B_E0;
DATA_INT <= '0';
एसीके <= '0';
और
मामला बी_सीएस है
जब B_E0 =>
IF (REQ ='1') तब B_NS <= B_E1;
ELSE B_NS <= B_E0;
अगर अंत;
DATA_INT <= '0';
एसीके <= '0';
जब B_E1 =>
IF (REQ ='1') तब B_NS <= B_E1;
ELSE B_NS <= B_E0;
अगर अंत;
DATA_INT <= DATA_IN;
एसीके <= '1';
अंत मामला;
अगर अंत;
प्रक्रिया समाप्त करें B_1;

बी_2: प्रक्रिया (सीके)
शुरू
अगर (सीके = '1' और सीके 'स्थिर नहीं)
फिर बी_सीएस <= बी_एनएस;
अगर अंत;
प्रक्रिया समाप्त करें B_2;

अंत एफएसएम;

सीटीएल उदाहरण

-- एक सीटीएल फ़ाइल उदाहरण

प्रकार A_ETAT_TYPE है (A_E0, A_E1);
प्रकार B_ETAT_TYPE है (B_E0, B_E1);

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

चर सीके: बिट;
चर डेटा_इन: बिट;
चर डेटा_आउट: बिट;
चर रीसेट: बिट;
चर एके: बिट;
चर अनुरोध: बिट;

RESET_COND init1: = (रीसेट = '1');
ASSUME ass1: = (रीसेट = '0');

शुरू करना

प्रोप1: पूर्व (एके = '1');
Prop2: एजी (req -> AF (एके));
प्रॉप4 : एयू (req='1', ack='1');

अंत;

कहवा उदाहरण

मोका-वी उदाहरण उदाहरण

onworks.net सेवाओं का उपयोग करके ऑनलाइन मोका का उपयोग करें