Project

General

Profile

EFSM Building » History » Version 3

Sergey Smolov, 07/18/2013 04:02 PM

1 1 Sergey Smolov
h1. EFSM Building (Алгоритм построения EFSM)
2
3
На вход алгоритму подаются:
4
5 3 Sergey Smolov
1. Граф зависимостей по данным (Data Flow Graph, DFG)
6
2. Список часов (clock-like variables) - сигналов, извлеченных алгоритмом Clock Extraction Algorithm
7 1 Sergey Smolov
8 3 Sergey Smolov
Алгоритм строит расширенный конечный автомат (Extended Finite State Machine, EFSM), представляющий собой набор вершин-состояний (State), связанных, быть может, ребрами-переходами (Transitions). Каждому состоянию взаимно однозначно соответствует ограничение на внутренние переменные (state constraint), а каждому переходу соответствует упорядоченный набор ограничений как на внутренние переменные, так и на входные и выходные сигналы (transition constraints).
9 1 Sergey Smolov
Алгоритм выполняет построение EFSM в несколько этапов:
10 2 Sergey Smolov
11 3 Sergey Smolov
1. Извлечение переменных состояния (state-like variables)
12
2. Проверка state-like variables на независимость
13
3. Построение набора ограничений на зависимые переменные состояния (state constraints) -> построение множества States
14 1 Sergey Smolov
4. Построение множества переходов Transitions
15
16
h2. Извлечение переменных состояния
17
18
Извлечение переменных состояния производится на основе анализа DFG. По определению, переменная state_var является переменной состояния, если:
19
20 3 Sergey Smolov
1. state-like variable не является входным сигналом;
21
2. В DFG существует Clocked Guarded Action 1 (CGA1), Guard которого содержит state-like variable, а clock нетривиален;
22
3. В DFG существует Clocked Guarded Action 2 (CGA2), Action которого содержит state_var, причем state_var принадлежит Def(Action);
23
4. В DFG существует путь *Path* из CCGA1 в CGA2;
24
5. В пути Path нет вершины, где задействован нетривиальный clock, не задействованный в CGA1\CGA2.
25 1 Sergey Smolov
26
h2. Проверка state vars на независимость
27
28 2 Sergey Smolov
Описанный выше критерий переменных состояния не исключает возможности существования в одном HDL-модуле более чем одной такой переменной. Следовательно, в рамках одного модуля возможно существование нескольких параллельно работающих EFSM. Необходимо установить соответствие между переменными состояния и EFSM. Если две переменные состояния являются независимыми, то им соответствуют разные EFSM. 
29
Для разбиения списка переменных состояния X на множества зависимых переменных X(i) применяется следующий подход. Каждой переменной состояния сопоставляется её *Path*. Для каждого *Path*  определяется, какие переменные состояния в нем задействованы, что позволяет сопоставить *Path* характеристический вектор длины n, где n - общее число переменных состояния (i-й элемент вектора равен TRUE если i-я переменная состояния задействована в данном пути, в противном случае I-й элемент вектора равен FALSE). В результате анализа всех путей получаем n*n-матрицу. 
30
Следующий шаг - построение множеств зависимых переменных. Делается это на основе сравнения строк матрицы - если в них есть совпадающие элементы (что соответствует факту участия одной и той же переменной состояния в разных *Path*), то две строки матрицы заменяются их дизъюнкцией. На выходе получается набор непересекающихся подмножеств множества переменных состояния.
31 1 Sergey Smolov
32
h2. Построение множества состояний
33
34 2 Sergey Smolov
На данном этапе обрабатывается набор охранных предикатов, включающих зависимые переменные состояния. Алгоритм строит из них набор ограничений, определяющих непресекающиеся множества значений переменных состояния. Ограничения строятся в виде всевозможных конъюнкций из полного числа охранных предикатов, либо их отрицаний. При генерации очередного ограничения выполняется его проверка на разрешимость, и если проверка завершилась вердиктом "да", то ограничение помещается в множество состояний EFSM.
35
36 1 Sergey Smolov
h2. Построение множества переходов
37
38 2 Sergey Smolov
На данном этапе обрабатываются множество состояний EFSM и множество CGA, которое состоит из двух подмножеств - CGA, содержащие переменные состояния в охранных предикатах (1), и не-содержащие переменных состояния в охранных предикатах (2). Сначала переходы строятся путем установления разрешимости ограничений, являющихся конъюнкциями состояний и охранных предикатов семейства (1) - это можно осуществить даже без использования решателя, если в ограничении на состояние хранить информацию о том, какие охранные предикаты при его конструировании были использованы с меткой "TRUE". В случае с охранными предикатами семейства (2) нужно задействовать решатель.
39
40
Если решатель завершил работу с вердиктом "да", то на основе соответствующего CGA (3) строится переход EFSM. В качестве конечной вершины перехода рассматриваются те CGA (4), в блоках действий которых присутствуют директивы записи в переменную состояния. Алгоритм ищет пути в DFG из (3) в (4) и, если таковой найден, помещает его в переход EFSM.
41
42
Далее решается проблема детерминизации EFSM. Алгоритм ищет такие ситуации, когда из одного исходного состояния EFSM есть два одинаковых перехода в разные конечные состояния EFSM. Для этого выполняется конструирование дополнительных условий на переходы путем "сворачивания" условий из конечный состояний с условиями, входящими в переход, в обратном порядке. На выходе получаем дополнительные условия, которые помещаются в начале переходов.