Retrascope

h1. 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

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

Извлечение переменных состояния производится на основе анализа 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.

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

Описанный выше критерий переменных состояния не исключает возможности существования в одном HDL-модуле более чем одной такой переменной. Следовательно, в рамках одного модуля возможно существование нескольких параллельно работающих EFSM. Необходимо установить соответствие между переменными состояния и EFSM. Если две переменные состояния являются независимыми, то им соответствуют разные EFSM. 

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

Следующий шаг - построение множеств зависимых переменных. Делается это на основе сравнения строк матрицы - если в них есть совпадающие элементы (что соответствует факту участия одной и той же переменной состояния в разных *Path*), то две строки матрицы заменяются их дизъюнкцией. На выходе получается набор непересекающихся подмножеств множества переменных состояния.

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

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

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

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

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

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