moka - מקוון בענן

תָכְנִית:

שֵׁם

MOKA - דגם בודק קדמון

תַקצִיר

מוקה [-VDB] fsm_filename ctl_filename

תיאור

מוקה הוא בודק מודל CTL.

נוצר כדי לרוץ על תיאורי FSM או RTL, מוקה תומך באותה תת-קבוצה של VHDL כמו syf או בום
(למידע נוסף על תת-קבוצה זו ראה SYF(1), בום(1), FSM(5), VBE(5)).
אף על פי כן מוקה כופה שלכל רישום של תיאור ההתנהגות יהיה אותו הדבר
מצב השעון ושאין אוטובוסים משולשים או מרובבים. במיוחד VHDL
סוג MUX_BIT ו-WOR_BIT אינם נתמכים.
קודם כל מוקה בנה את מעבר הפונקציות של ה-FSM באמצעות בינארי מופחת מסדר
ייצוג דיאגרמות החלטה.
לאחר מכן הוא מחיל את התנאים הראשוניים כדי למצוא את המצב הראשון (מילת מפתח INITIAL ו/או
RESET_COND ב CTL(5) פורמט קובץ).
לאחר שהוא מחשב הדמיה סמלית של FSM על מנת למצוא את כל המצבים שניתן להגיע אליהם.
חישוב זה לוקח בחשבון את תנאי ההנחות (מילת מפתח ASSUME ב-
CTL(5) פורמט קובץ).
מוקה מאמת לבסוף אחד אחד כל נוסחאות CTL. (לִרְאוֹת CTL(5) עבור פורמט קובץ CTL
פרטים).

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 תמיד
נכון.

הסביבה וריאציות

MBK_WORK_LIB נותן את הנתיב לתיאור ולקובץ CTL. ערך ברירת המחדל הוא
הספרייה הנוכחית.

MBK_CATA_LIB נותן כמה נתיבים עזר לתיאורים ולקובץ CTL. ה
ערך ברירת המחדל הוא הספרייה הנוכחית.

אפשרויות

-V מפעיל מצב מילולי. כל שלב בבדיקת הדגם מוצג בתקן
פלט.

-D מפעיל את מצב ניפוי באגים. כל שלב בבדיקת המודל מפורט על הפלט הסטנדרטי.
בפרט כל המצבים שנקבעו מוצגים עבור כל תת-ביטוי CTL.

-B קובץ הקלט הוא תיאור VHDL באמצעות קבוצת המשנה של Alliance VHDL (ראה VBE(5) קובץ
תבנית).

FSM דוגמא

-- דוגמה רב fsm

דוגמה ENTITY היא
נמל
(
ck : ב-BIT;
data_in : ב-BIT;
איפוס: ב-BIT;
data_out : החוצה BIT
);
דוגמה END;

ארכיטקטורה FSM של דוגמה היא

TYPE A_ETAT_TYPE IS (A_E0, A_E1);
SIGNAL 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
--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;

התחל

A_1 : PROCESS ( A_CS, ACK )
התחל
IF (איפוס = '1')
THEN A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
אחר
CASE A_CS הוא
כאשר A_E0 =>
IF ( ACK ='1') THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
הסוף אם;
DATA_OUT <= '0';
REQ <= '1';
כאשר A_E1 =>
IF ( ACK ='1') THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
הסוף אם;
DATA_OUT <= DATA_INT;
REQ <= '0';
מקרה סיום;
הסוף אם;
סיום תהליך A_1;

A_2: PROCESS( ck)
התחל
IF ( ck = '1' ולא ck'Stable )
THEN A_CS <= A_NS;
הסוף אם;
סיום תהליך A_2;

-------

B_1 : PROCESS ( B_CS, ACK )
התחל
IF (איפוס = '1')
THEN B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
אחר
CASE B_CS הוא
כאשר B_E0 =>
IF ( REQ ='1') THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
הסוף אם;
DATA_INT <= '0';
ACK <= '0';
כאשר B_E1 =>
IF ( REQ ='1') THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
הסוף אם;
DATA_INT <= DATA_IN;
ACK <= '1';
מקרה סיום;
הסוף אם;
סיום תהליך B_1;

B_2: PROCESS( ck)
התחל
IF ( ck = '1' ולא ck'Stable )
THEN B_CS <= B_NS;
הסוף אם;
סיום תהליך B_2;

END FSM;

CTL דוגמא

-- דוגמה לקובץ CTL

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

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

משתנה ck : BIT;
VARIABLE data_in : BIT;
VARIABLE data_out : BIT;
איפוס משתנה: BIT;
ACK משתנה: BIT;
דרישת משתנה: BIT;

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

להתחיל

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

הסוף;

מוצ'ה דוגמא

moka -V לדוגמה

השתמש במוקה באינטרנט באמצעות שירותי onworks.net