EFSM Building » History » Revision 5
Revision 4 (Sergey Smolov, 07/18/2013 05:23 PM) → Revision 5/6 (Alexander Kamkin, 01/17/2014 04:42 PM)
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_ ≠ _y_) → ¬(_x_ = _y_), (_x_ ≥ _y_) → ¬(_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~) множество состояний EFSM. h2. Построение множества переходов На данном этапе обрабатываются множество состояний EFSM и множество CGA, которое состоит из двух подмножеств - CGA, содержащие переменные состояния в охранных предикатах (1), и не-содержащие переменных состояния в охранных предикатах (2). Сначала переходы строятся путем установления разрешимости ограничений, являющихся конъюнкциями состояний и охранных предикатов семейства (1) - это можно осуществить даже без использования решателя, если в ограничении на состояние хранить информацию о том, какие охранные предикаты при его конструировании были использованы с меткой "TRUE". В случае с охранными предикатами семейства (2) нужно задействовать решатель. Если решатель завершил работу с вердиктом "да", то на основе соответствующего CGA (3) строится переход EFSM. В качестве конечной вершины перехода рассматриваются те CGA (4), в блоках действий которых присутствуют директивы записи в переменную состояния. Алгоритм ищет пути в DFG из (3) в (4) и, если таковой найден, помещает его в переход EFSM. Далее решается проблема детерминизации EFSM. Алгоритм ищет такие ситуации, когда из одного исходного состояния EFSM есть два одинаковых перехода в разные конечные состояния EFSM. Для этого выполняется конструирование дополнительных условий на переходы путем "сворачивания" условий из конечный состояний с условиями, входящими в переход, в обратном порядке. На выходе получаем дополнительные условия, которые помещаются в начале переходов.