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.

На предварительном этапе все условия, входящие в ограничения, записываются в канонической форме – удаляется избыточность: (_x_ &ne; _y_) &rarr; &not;(_x_ = _y_), (_x_ &ge; _y_) &rarr; &not;(_x_ < _y_) и т.п. После этого, каждому атому (элементарной логической формуле) ставится в соответствие булева переменная, а дальнейший анализ осуществляется в терминах алгебры логики. Заметим, что если часть атомов используется только в составе некоторой подформулы, имеет смысл сопоставить булеву переменную сразу всей этой подформуле.

Пусть каждое ограничение представлено в форме конъюнкции литералов (переменных или их отрицаний). Если это не так, видимо, ограничение нужно расщеплять – приводить к ДНФ (или представлять в форме BDD). Задача – проверить попарную ортогональность ограничений и, если ее нет, провести ортогонализацию. Ортогональность двух конъюнкций определяется наличием переменной, которая входит в одну из них без отрицания, а в другую – с отрицанием. Ортогонализация выполняется следующим образом. Пусть (_x_ ~1~ … _x_ ~n~ Φ) и (_y_ ~1~ … _y_ ~m~ Φ) – два неортогональных ограничения (для краткости знак конъюнкции опущен), где Φ – их общая подформула (возможно пустая), переменные, входящие в литералы _x_ ~i~ и _y_ ~j~, попарно различны, и хотя бы одно из множеств { _x_ ~i~ } или { _y_ ~j~ } не пусто. Тогда, в результате ортогонализации будут получены, например, следующие ограничения:

* (_x_ ~1~ … _x_ ~n~ Φ)

* (_y_ ~1~ … _y_ ~m~ Φ)(¬ _x_ ~1~)

* (_y_ ~1~ … _y_ ~m~ Φ)(_x_ ~1~ ¬ _x_ ~2~)

* ...

* (_y_ ~1~ … _y_ ~m~ Φ)(_x_ ~1~ _x_ ~2~ ... _x_ ~n-1~ ¬ _x_ ~n~)

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

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

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

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