Project

General

Profile

EFSM Building » History » Version 6

Alexander Kamkin, 01/17/2014 04:51 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 Sergey Smolov
4. В DFG существует путь Path из CCGA1 в CGA2;
24 3 Sergey Smolov
5. В пути Path нет вершины, где задействован нетривиальный clock, не задействованный в CGA1\CGA2.
25 1 Sergey Smolov
26
h2. Проверка state vars на независимость
27
28 2 Sergey Smolov
Описанный выше критерий переменных состояния не исключает возможности существования в одном HDL-модуле более чем одной такой переменной. Следовательно, в рамках одного модуля возможно существование нескольких параллельно работающих EFSM. Необходимо установить соответствие между переменными состояния и EFSM. Если две переменные состояния являются независимыми, то им соответствуют разные EFSM. 
29 4 Sergey Smolov
Для разбиения списка переменных состояния 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 5 Alexander Kamkin
На данном этапе обрабатывается множество ограничений (охранных условий и постусловий действий), включающих зависимые переменные состояния. Цель – ортогонализировать множество ограничений, т.е. уточнить/разбить некоторые ограничения таким образом, чтобы в результате ограничения оказались попарно несовместными. Каждое из полученных ограничений соответствует состоянию EFSM.
35
36
На предварительном этапе все условия, входящие в ограничения, записываются в канонической форме – удаляется избыточность: (_x_ &ne; _y_) &rarr; &not;(_x_ = _y_), (_x_ &ge; _y_) &rarr; &not;(_x_ < _y_) и т.п. После этого, каждому атому (элементарной логической формуле) ставится в соответствие булева переменная, а дальнейший анализ осуществляется в терминах алгебры логики. Заметим, что если часть атомов используется только в составе некоторой подформулы, имеет смысл сопоставить булеву переменную сразу всей этой подформуле.
37
38 6 Alexander Kamkin
Пусть каждое ограничение представлено в форме конъюнкции литералов (переменных или их отрицаний). Если это не так, видимо, ограничение нужно расщеплять – приводить к ДНФ. Задача – проверить попарную ортогональность ограничений и, если ее нет, провести ортогонализацию. Ортогональность двух конъюнкций определяется наличием переменной, которая входит в одну из них без отрицания, а в другую – с отрицанием. Ортогонализация выполняется следующим образом. Пусть (_x_ ~1~ … _x_ ~n~ &Phi;) и (_y_ ~1~ … _y_ ~m~ &Phi;) – два неортогональных ограничения (для краткости знак конъюнкции опущен), где &Phi; – их общая подформула (возможно пустая), переменные, входящие в литералы _x_ ~i~ и _y_ ~j~, попарно различны, и хотя бы одно из множеств { _x_ ~i~ } или { _y_ ~j~ } не пусто. Тогда, в результате ортогонализации будут получены, например, следующие ограничения:
39 5 Alexander Kamkin
40
* (_x_ ~1~ … _x_ ~n~ &Phi;)
41
* (_y_ ~1~ … _y_ ~m~ &Phi;)(&not; _x_ ~1~)
42
* (_y_ ~1~ … _y_ ~m~ &Phi;)(_x_ ~1~ &not; _x_ ~2~)
43
* ...
44 1 Sergey Smolov
* (_y_ ~1~ … _y_ ~m~ &Phi;)(_x_ ~1~ _x_ ~2~ ... _x_ ~n-1~ &not; _x_ ~n~)
45 6 Alexander Kamkin
46
Другой способ – построить BDD для дизъюнкции всех ограничений. В этом случае конъюнкции, задаваемые путями от корня BDD к листу 1 ортогональны. Каждая из них соответствует состоянию EFSM.
47 2 Sergey Smolov
48 1 Sergey Smolov
h2. Построение множества переходов
49
50 2 Sergey Smolov
На данном этапе обрабатываются множество состояний EFSM и множество CGA, которое состоит из двух подмножеств - CGA, содержащие переменные состояния в охранных предикатах (1), и не-содержащие переменных состояния в охранных предикатах (2). Сначала переходы строятся путем установления разрешимости ограничений, являющихся конъюнкциями состояний и охранных предикатов семейства (1) - это можно осуществить даже без использования решателя, если в ограничении на состояние хранить информацию о том, какие охранные предикаты при его конструировании были использованы с меткой "TRUE". В случае с охранными предикатами семейства (2) нужно задействовать решатель.
51
52
Если решатель завершил работу с вердиктом "да", то на основе соответствующего CGA (3) строится переход EFSM. В качестве конечной вершины перехода рассматриваются те CGA (4), в блоках действий которых присутствуют директивы записи в переменную состояния. Алгоритм ищет пути в DFG из (3) в (4) и, если таковой найден, помещает его в переход EFSM.
53
54
Далее решается проблема детерминизации EFSM. Алгоритм ищет такие ситуации, когда из одного исходного состояния EFSM есть два одинаковых перехода в разные конечные состояния EFSM. Для этого выполняется конструирование дополнительных условий на переходы путем "сворачивания" условий из конечный состояний с условиями, входящими в переход, в обратном порядке. На выходе получаем дополнительные условия, которые помещаются в начале переходов.