moka - онлайн в хмарі

ПРОГРАМА:

ІМ'Я

MOKA - Модель шашка предка

СИНТАКСИС

кава мокко [-VDB] ім'я_файлу fsm ctl_ім'я_файлу

ОПИС

кава мокко це засіб перевірки CTL моделі.

Розроблено для роботи з описами FSM або RTL, кава мокко підтримує ту саму підмножину VHDL, що й syf або boom
(додаткову інформацію про цю підмножину див SYF(1) BOOM(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. The
значенням за замовчуванням є поточний каталог.

ВАРІАНТИ

-V Вмикає докладний режим. Кожен крок перевірки моделі відображається на стандарті
вихід.

-D Вмикає режим налагодження. Кожен крок перевірки моделі детально описано на стандартному виводі.
Зокрема, для кожного підвиразу CTL відображаються всі набір станів.

-B Вхідний файл є описом VHDL з використанням підмножини VHDL Alliance (див VBE(5) файл
формат).

FSM приклад

-- Приклад мульти fsm

Приклад ENTITY
PORT
(
ck : у BIT;
data_in : у BIT;
скидання : в BIT;
data_out : вихід BIT
);
приклад END;

АРХІТЕКТУРА FSM OF наприклад

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

SIGNAL ACK, REQ, DATA_INT : BIT;

ПОЧАТИ

A_1: ПРОЦЕС (A_CS, ACK)
ПОЧАТИ
ЯКЩО (скидання = '1')
THEN A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ELSE
CASE A_CS є
КОЛИ A_E0 =>
IF ( ACK ='1'), THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
END IF;
DATA_OUT <= '0';
REQ <= '1';
КОЛИ A_E1 =>
IF ( ACK ='1'), THEN A_NS <= A_E1;
ELSE A_NS <= A_E0;
END IF;
DATA_OUT <= DATA_INT;
REQ <= '0';
КІНЦЕВА СПРАВА;
END IF;
ЗАВЕРШИТИ ПРОЦЕС A_1;

A_2 : ПРОЦЕС ( ck )
ПОЧАТИ
ЯКЩО ( ck = '1' І НЕ ck' STABLE )
THEN A_CS <= A_NS;
END IF;
ЗАВЕРШИТИ ПРОЦЕС A_2;

-------

B_1: ПРОЦЕС (B_CS, ACK)
ПОЧАТИ
ЯКЩО (скидання = '1')
THEN B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
ELSE
CASE B_CS є
КОЛИ B_E0 =>
IF ( REQ ='1'), THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DATA_INT <= '0';
ACK <= '0';
КОЛИ B_E1 =>
IF ( REQ ='1'), THEN B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DATA_INT <= DATA_IN;
ACK <= '1';
КІНЦЕВА СПРАВА;
END IF;
ЗАВЕРШЕННЯ ПРОЦЕС B_1;

B_2 : ПРОЦЕС ( ck )
ПОЧАТИ
ЯКЩО ( ck = '1' І НЕ ck' STABLE )
THEN B_CS <= B_NS;
END IF;
ЗАВЕРШЕННЯ ПРОЦЕС 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 : БІТ;
VARIABLE data_in : BIT;
VARIABLE data_out : BIT;
скидання змінної: BIT;
VARIABLE ack: BIT;
VARIABLE req : BIT;

RESET_COND init1 := (скидання='1');
ПРИЙМАТИ ass1 := (скидання='0');

починати

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

end;

МОКА приклад

moka -V приклад приклад

Використовуйте moka онлайн за допомогою служб onworks.net