এটি মোকা কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।
কার্যক্রম:
NAME এর
MOKA - মডেল চেকার পূর্বপুরুষ
সাইনোপিসিস
Moka [-ভিডিবি] fsm_filename ctl_filename
বর্ণনাঃ
Moka একটি CTL মডেল পরীক্ষক।
FSM বা RTL বিবরণে চালানোর জন্য তৈরি করা হয়েছে, Moka syf বা বুমের মতো একই VHDL উপসেট সমর্থন করে
(এই উপসেট সম্পর্কে আরও তথ্যের জন্য দেখুন SYF(২০১১), গম্ভীর গর্জন(২০১১), FSM(২০১১), VBE(5))।
তবু Moka আরোপ করে যে আচরণগত বর্ণনার প্রতিটি রেজিস্টারে একই রকম আছে
ঘড়ির অবস্থা এবং কোন ট্রাস্টেট বা মাল্টিপ্লেক্স বাস নেই। বিশেষ করে ভিএইচডিএল
টাইপ MUX_BIT এবং WOR_BIT সমর্থিত নয়৷
প্রথম সব Moka একটি হ্রাসকৃত আদেশকৃত বাইনারি ব্যবহার করে FSM এর ফাংশন রূপান্তর তৈরি করুন
সিদ্ধান্ত ডায়াগ্রাম প্রতিনিধিত্ব.
এটি তারপর প্রথম অবস্থা (কিওয়ার্ড প্রাথমিক এবং/অথবা) খুঁজে পেতে প্রাথমিক শর্তগুলি প্রয়োগ করে
RESET_COND এর মধ্যে সিটিএল(5) ফাইল বিন্যাস)।
এটি সমস্ত পৌঁছানো যায় এমন অবস্থা খুঁজে পেতে FSM-এর একটি প্রতীকী সিমুলেশন গণনা করার পরে।
এই গণনাটি অনুমানের শর্তগুলিকে বিবেচনা করে (এতে কীওয়ার্ড ASSUME
সিটিএল(5) ফাইল বিন্যাস)।
Moka অবশেষে প্রতিটি সিটিএল সূত্র একে একে যাচাই করে। (দেখা সিটিএল(5) CTL ফাইল ফরম্যাটের জন্য
বিস্তারিত)।
সিটিএল অপারেটর
প্রতিটি CTL সাব-এক্সপ্রেশনের জন্য Moka ফর্মুলা যাচাই করে এমন রাজ্যের সেট ফিরিয়ে দেবে।
যেমন EX(p) EX(p) যাচাই করে এমন পৌঁছানো যায় এমন অবস্থার সেট ফিরিয়ে দেবে।
সিটিএল অপারেটর:
EX(p): এমন সমস্ত রাজ্য ফেরত দেয় যার প্রায় একটি প্রাথমিক রাজ্য উত্তরসূরি রয়েছে
যাচাই করে p.
EU(p,q): প্রায় একটি পথের মূল এমন সমস্ত রাজ্য প্রদান করে, যেমন p is
পর্যন্ত সত্য q সর্বদা সত্য।
EG(p): প্রায় একটি পথের মূল এমন সমস্ত অবস্থা প্রদান করে, যেমন p is
সবসময় সত্য.
AX(p) : এমন সমস্ত রাজ্যকে ফেরত দেয় যেগুলির সমস্ত প্রাথমিক রাজ্য উত্তরসূরি রয়েছে৷
যাচাই করে p.
AU(p,q) : এমন সমস্ত অবস্থা প্রদান করে যেগুলি থেকে শুধুমাত্র পথের মূল p সত্য
পর্যন্ত q সর্বদা সত্য।
AG(p): শুধুমাত্র পথের মূল এমন সমস্ত অবস্থা প্রদান করে, যেমন p সবসময়
সত্য।
পরিবেশ বৈচিত্র্য
MBK_WORK_LIB বর্ণনা এবং CTL ফাইলের জন্য পথ দেয়। ডিফল্ট মান হল
বর্তমান ডিরেক্টরি।
MBK_CATA_LIB বর্ণনা এবং CTL ফাইলের জন্য কিছু সহায়ক পথ দেয়। দ্য
ডিফল্ট মান হল বর্তমান ডিরেক্টরি।
বিকল্প
-V ভার্বোজ মোড চালু করে। মডেল চেকিংয়ের প্রতিটি ধাপ স্ট্যান্ডার্ডে প্রদর্শিত হয়
আউটপুট।
-D ডিবাগ মোড চালু করে। মডেল চেকিং প্রতিটি ধাপ স্ট্যান্ডার্ড আউটপুট বিস্তারিত.
বিশেষ করে প্রতিটি CTL সাব-এক্সপ্রেশনের জন্য সমস্ত স্টেট সেট প্রদর্শিত হয়।
-বি ইনপুট ফাইলটি অ্যালায়েন্স ভিএইচডিএল উপসেট ব্যবহার করে একটি VHDL বিবরণ (দেখুন VBE(5) ফাইল
বিন্যাস)।
FSM EXAMPLE টি
-- একটি মাল্টি এফএসএম উদাহরণ
ENTITY উদাহরণ হল
পোর্ট
(
ck: বিআইটিতে;
ডেটা_ইন : বিআইটিতে;
রিসেট: বিআইটিতে;
ডাটা_আউট : বিট আউট
);
শেষ উদাহরণ;
আর্কিটেকচার এফএসএম এর উদাহরণ
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);
SIGNAL B_NS, B_CS : B_ETAT_TYPE;
--PRAGMA CURRENT_STATE A_CS FSM_A
--PRAGMA NEXT_STATE A_NS FSM_A
--প্রগমা ঘড়ি ck FSM_A
--PRAGMA FIRST_STATE A_E0 FSM_A
--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--প্রগমা ঘড়ি ck FSM_B
--PRAGMA FIRST_STATE B_E0 FSM_B
সিগন্যাল ACK, REQ, DATA_INT : BIT;
BEGIN
A_1 : প্রক্রিয়া ( A_CS, ACK )
BEGIN
যদি (রিসেট = '1')
তারপর A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ছাড়া আর অন্য
CASE A_CS হল
WHEN A_E0 =>
যদি ( ACK ='1') তাহলে A_NS <= A_E1;
ELSE A_NS <= A_E0;
যদি শেষ;
DATA_OUT <= '0';
REQ <= '1';
WHEN A_E1 =>
যদি ( ACK ='1') তাহলে A_NS <= A_E1;
ELSE A_NS <= A_E0;
যদি শেষ;
DATA_OUT <= DATA_INT;
REQ <= '0';
সমাপ্তি কেস;
যদি শেষ;
শেষ প্রক্রিয়া A_1;
A_2 : প্রক্রিয়া ( ck )
BEGIN
যদি ( ck = '1' এবং ck' স্থিতিশীল নয়)
তারপর A_CS <= A_NS;
যদি শেষ;
শেষ প্রক্রিয়া A_2;
-------
B_1 : প্রক্রিয়া ( B_CS, ACK )
BEGIN
যদি (রিসেট = '1')
তারপর B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
ছাড়া আর অন্য
CASE B_CS হল
WHEN B_E0 =>
যদি ( REQ ='1') তাহলে B_NS <= B_E1;
ELSE B_NS <= B_E0;
যদি শেষ;
DATA_INT <= '0';
ACK <= '0';
WHEN B_E1 =>
যদি ( REQ ='1') তাহলে B_NS <= B_E1;
ELSE B_NS <= B_E0;
যদি শেষ;
DATA_INT <= DATA_IN;
ACK <= '1';
সমাপ্তি কেস;
যদি শেষ;
শেষ প্রক্রিয়া B_1;
B_2 : প্রক্রিয়া ( ck )
BEGIN
যদি ( ck = '1' এবং ck' স্থিতিশীল নয়)
তারপর B_CS <= B_NS;
যদি শেষ;
শেষ প্রক্রিয়া B_2;
শেষ FSM;
সিটিএল EXAMPLE টি
-- একটি 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;
পরিবর্তনশীল ck : BIT;
variable data_in : BIT;
পরিবর্তনশীল ডেটা_আউট : বিট;
পরিবর্তনশীল রিসেট: বিট;
পরিবর্তনশীল ack : বিট;
পরিবর্তনশীল অনুরোধ : বিট;
RESET_COND init1 := (রিসেট='1');
ধরে নিন ass1 := (রিসেট='0');
শুরু করা
prop1 : EX( ack='1');
prop2 : AG( req -> AF( ack ) );
prop4 : AU(req='1', ack='1');
শেষ;
MOCHA EXAMPLE টি
moka -V উদাহরণ উদাহরণ
onworks.net পরিষেবা ব্যবহার করে অনলাইনে মোকা ব্যবহার করুন
