EFSM Building (Алгоритм построения EFSM)¶

На вход алгоритму подаются:

1. Граф зависимостей по данным (Data Flow Graph, DFG)
2. Список часов (clock-like variables) - сигналов, извлеченных алгоритмом Clock Extraction Algorithm

Алгоритм строит расширенный конечный автомат (Extended Finite State Machine, EFSM), представляющий собой набор вершин-состояний (State), связанных, быть может, ребрами-переходами (Transitions). Каждому состоянию взаимно однозначно соответствует ограничение на внутренние переменные (state constraint), а каждому переходу соответствует упорядоченный набор ограничений как на внутренние переменные, так и на входные и выходные сигналы (transition constraints).
Алгоритм выполняет построение EFSM в несколько этапов:

1. Извлечение переменных состояния (state-like variables)
2. Проверка state-like variables на независимость
3. Построение набора ограничений на зависимые переменные состояния (state constraints) -> построение множества States
4. Построение множества переходов Transitions

Извлечение переменных состояния¶

Извлечение переменных состояния производится на основе анализа DFG. По определению, переменная state_var является переменной состояния, если:

1. state-like variable не является входным сигналом;
2. В DFG существует Clocked Guarded Action 1 (CGA1), Guard которого содержит state-like variable, а clock нетривиален;
3. В DFG существует Clocked Guarded Action 2 (CGA2), Action которого содержит state_var, причем state_var принадлежит Def(Action);
4. В DFG существует путь Path из CCGA1 в CGA2;
5. В пути Path нет вершины, где задействован нетривиальный clock, не задействованный в CGA1\CGA2.

Проверка state vars на независимость¶

Описанный выше критерий переменных состояния не исключает возможности существования в одном HDL-модуле более чем одной такой переменной. Следовательно, в рамках одного модуля возможно существование нескольких параллельно работающих EFSM. Необходимо установить соответствие между переменными состояния и EFSM. Если две переменные состояния являются независимыми, то им соответствуют разные EFSM.
Для разбиения списка переменных состояния X на множества зависимых переменных X(i) применяется следующий подход. Каждой переменной состояния сопоставляется её Path. Для каждого Path определяется, какие переменные состояния в нем задействованы, что позволяет сопоставить Path характеристический вектор длины n, где n - общее число переменных состояния (i-й элемент вектора равен TRUE если i-я переменная состояния задействована в данном пути, в противном случае I-й элемент вектора равен FALSE). В результате анализа всех путей получаем n*n-матрицу.
Следующий шаг - построение множеств зависимых переменных. Делается это на основе сравнения строк матрицы - если в них есть совпадающие элементы (что соответствует факту участия одной и той же переменной состояния в разных Path), то две строки матрицы заменяются их дизъюнкцией. На выходе получается набор непересекающихся подмножеств множества переменных состояния.

Построение множества состояний¶

На данном этапе обрабатывается множество ограничений (охранных условий и постусловий действий), включающих зависимые переменные состояния. Цель – ортогонализировать множество ограничений, т.е. уточнить/разбить некоторые ограничения таким образом, чтобы в результате ограничения оказались попарно несовместными. Каждое из полученных ограничений соответствует состоянию EFSM.

На предварительном этапе все условия, входящие в ограничения, записываются в канонической форме – удаляется избыточность: (x ≠ y) → ¬(x = y), (x ≥ y) → ¬(x < y) и т.п. После этого, каждому атому (элементарной логической формуле) ставится в соответствие булева переменная, а дальнейший анализ осуществляется в терминах алгебры логики. Заметим, что если часть атомов используется только в составе некоторой подформулы, имеет смысл сопоставить булеву переменную сразу всей этой подформуле.

Пусть каждое ограничение представлено в форме конъюнкции литералов (переменных или их отрицаний). Если это не так, видимо, ограничение нужно расщеплять – приводить к ДНФ (или представлять в форме BDD). Задача – проверить попарную ортогональность ограничений и, если ее нет, провести ортогонализацию. Ортогональность двух конъюнкций определяется наличием переменной, которая входит в одну из них без отрицания, а в другую – с отрицанием. Ортогонализация выполняется следующим образом. Пусть (x ₁ … x _n Φ) и (y ₁ … y _m Φ) – два неортогональных ограничения (для краткости знак конъюнкции опущен), где Φ – их общая подформула (возможно пустая), переменные, входящие в литералы x _i и y _j, попарно различны, и хотя бы одно из множеств { x _i } или { y _j } не пусто. Тогда, в результате ортогонализации будут получены, например, следующие ограничения:

• (x ₁ … x _n Φ)
• (y ₁ … y _m Φ)(¬ x ₁)
• (y ₁ … y _m Φ)(x ₁ ¬ x ₂)
• ...
• (y ₁ … y _m Φ)(x ₁ x ₂ ... x _n-1 ¬ x _n)

Построение множества переходов¶

На данном этапе обрабатываются множество состояний EFSM и множество CGA, которое состоит из двух подмножеств - CGA, содержащие переменные состояния в охранных предикатах (1), и не-содержащие переменных состояния в охранных предикатах (2). Сначала переходы строятся путем установления разрешимости ограничений, являющихся конъюнкциями состояний и охранных предикатов семейства (1) - это можно осуществить даже без использования решателя, если в ограничении на состояние хранить информацию о том, какие охранные предикаты при его конструировании были использованы с меткой "TRUE". В случае с охранными предикатами семейства (2) нужно задействовать решатель.

Если решатель завершил работу с вердиктом "да", то на основе соответствующего CGA (3) строится переход EFSM. В качестве конечной вершины перехода рассматриваются те CGA (4), в блоках действий которых присутствуют директивы записи в переменную состояния. Алгоритм ищет пути в DFG из (3) в (4) и, если таковой найден, помещает его в переход EFSM.

Далее решается проблема детерминизации EFSM. Алгоритм ищет такие ситуации, когда из одного исходного состояния EFSM есть два одинаковых перехода в разные конечные состояния EFSM. Для этого выполняется конструирование дополнительных условий на переходы путем "сворачивания" условий из конечный состояний с условиями, входящими в переход, в обратном порядке. На выходе получаем дополнительные условия, которые помещаются в начале переходов.