moka - Интернет в облаке

ПРОГРАММА:

ИМЯ

MOKA - предок модельного шашечка

СИНТАКСИС

кофе мокко [-ВДБ] fsm_filename ctl_filename

ОПИСАНИЕ

кофе мокко это программа для проверки моделей CTL.

Создан для работы с описаниями FSM или RTL, кофе мокко поддерживает то же подмножество VHDL, что и syf или boom
(для получения дополнительной информации об этом подмножестве см. SYF(1) BOOM(1) ФШМ(5) VBE(5)).
Тем не менее кофе мокко требует, чтобы каждый регистр описания поведения имел одинаковые
состояние часов и что нет трехсторонних или мультиплексированных шин. В частности VHDL
типы MUX_BIT и WOR_BIT не поддерживаются.
Прежде всего кофе мокко построить функциональный переход конечного автомата, используя сокращенный упорядоченный двоичный
Представление схем принятия решений.
Затем он применяет начальные условия, чтобы найти первое состояние (ключевое слово INITIAL и / или
RESET_COND в CTL(5) формат файла).
После этого он вычисляет символьное моделирование конечного автомата, чтобы найти все достижимые состояния.
Это вычисление учитывает условия предположений (ключевое слово 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) файл
формат).

ФШМ ПРИМЕР

- Пример мультифсм

Пример ENTITY:
PORT
(
ck: в BIT;
data_in: в BIT;
сброс: в BIT;
data_out: out BIT
);
END пример;

АРХИТЕКТУРА FSM примера

ТИП A_ETAT_TYPE IS (A_E0, A_E1);
СИГНАЛ A_NS, A_CS: A_ETAT_TYPE;

ТИП B_ETAT_TYPE IS (B_E0, B_E1);
СИГНАЛ B_NS, B_CS: B_ETAT_TYPE;

--PRAGMA ТЕКУЩЕЕ_СОСТОЯНИЕ A_CS FSM_A
--PRAGMA NEXT_STATE A_NS FSM_A
- ЧАСЫ PRAGMA ck FSM_A
--ПРАГМА ПЕРВОЕ_СОСТОЯНИЕ A_E0 FSM_A

--PRAGMA ТЕКУЩЕЕ_СОСТОЯНИЕ B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
- ЧАСЫ PRAGMA ck FSM_B
--ПРАГМА ПЕРВОЕ_СОСТОЯНИЕ B_E0 FSM_B

СИГНАЛ ACK, REQ, DATA_INT: BIT;

НАЧАТЬ

A_1: ПРОЦЕСС (A_CS, ACK)
НАЧАТЬ
ЕСЛИ (сброс = '1')
ТОГДА A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ELSE
CASE A_CS - это
КОГДА A_E0 =>
ЕСЛИ (ACK = '1') ТОГДА A_NS <= A_E1;
ИНАЧЕ A_NS <= A_E0;
END IF;
DATA_OUT <= '0';
REQ <= '1';
КОГДА A_E1 =>
ЕСЛИ (ACK = '1') ТОГДА A_NS <= A_E1;
ИНАЧЕ A_NS <= A_E0;
END IF;
DATA_OUT <= DATA_INT;
REQ <= '0';
КОНЕЦ ДЕЛА;
END IF;
КОНЕЦ ПРОЦЕССА A_1;

A_2: ПРОЦЕСС (ck)
НАЧАТЬ
ЕСЛИ (ck = '1' И НЕ ck'STABLE)
ТОГДА A_CS <= A_NS;
END IF;
КОНЕЦ ПРОЦЕССА A_2;

-------

B_1: ПРОЦЕСС (B_CS, ACK)
НАЧАТЬ
ЕСЛИ (сброс = '1')
ТОГДА B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
ELSE
CASE B_CS - это
КОГДА B_E0 =>
ЕСЛИ (REQ = '1') ТОГДА B_NS <= B_E1;
ИНАЧЕ B_NS <= B_E0;
END IF;
DATA_INT <= '0';
ACK <= '0';
КОГДА B_E1 =>
ЕСЛИ (REQ = '1') ТОГДА B_NS <= B_E1;
ИНАЧЕ B_NS <= B_E0;
END IF;
DATA_INT <= DATA_IN;
ACK <= '1';
КОНЕЦ ДЕЛА;
END IF;
КОНЕЦ ПРОЦЕССА B_1;

B_2: ПРОЦЕСС (ck)
НАЧАТЬ
ЕСЛИ (ck = '1' И НЕ ck'STABLE)
ТОГДА B_CS <= B_NS;
END IF;
КОНЕЦ ПРОЦЕССА B_2;

КОНЕЦ FSM;

CTL ПРИМЕР

- Пример файла CTL

ТИП A_ETAT_TYPE IS (A_E0, A_E1);
ТИП B_ETAT_TYPE IS (B_E0, B_E1);

ПЕРЕМЕННАЯ A_NS, A_CS: A_ETAT_TYPE;
ПЕРЕМЕННАЯ B_NS, B_CS: B_ETAT_TYPE;

ПЕРЕМЕННАЯ ck: BIT;
ПЕРЕМЕННАЯ data_in: BIT;
ПЕРЕМЕННАЯ data_out: BIT;
ПЕРЕМЕННАЯ сброс: BIT;
ПЕРЕМЕННАЯ ack: BIT;
ПЕРЕМЕННАЯ req: BIT;

RESET_COND init1: = (сброс = '1');
ПРИНЯТЬ ass1: = (reset = '0');

начинать

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

конец;

MOKA ПРИМЕР

moka -V пример примера

Используйте moka в Интернете с помощью сервисов onworks.net