Retrascope

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

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

1. Граф зависимостей по данным (Data Flow Graph, **DFG**)

2. Список часов (**clocks**) - сигналов, извлеченных алгоритмом Clock Extraction Algorithm

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

Алгоритм выполняет построение EFSM в несколько этапов:

1. Извлечение переменных состояния (**state vars**)

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

3. Построение набора ограничений на зависимые переменные состояния (state constraints) -> построение множества States

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

5. Проверка Transitions на независимость/совместимость со state constraints

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

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

1. state_var не является входным сигналом (input signal, input)

2. В DFG существует Guarded Action 1, Guard которого содержит state_var, а также содержит некоторый clock (state_var, clock принадлежат Use(Guard))

3. В DFG существует Guarded Action 2, Action которого содержит state_var, причем state_var принадлежит Def(Action)

4. В DFG существует путь Path из Guarded Action 1 в Guarded Action 2

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

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

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

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

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

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

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