Project

General

Profile

EFSM Building (Related Work) » History » Version 22

Sergey Smolov, 03/29/2017 05:18 PM

1 1 Sergey Smolov
h1. EFSM Building (Related Work)
2
3 22 Sergey Smolov
Алгоритмы извлечения EFSM-моделей из исходного кода HDL-описаний. Все перечисленные методы строят по одному EFSM на каждый процесс целевого HDL-описания.
4 1 Sergey Smolov
5 22 Sergey Smolov
{{toc}}
6
7 17 Sergey Smolov
h2. Giomi J.-C. 1995 Finite State Machine Extraction From Hardware Description Languages
8 16 Sergey Smolov
9 10 Sergey Smolov
Алгоритм строит FSM-модели - частный случай EFSM-моделей - по HDL-описанию.
10 1 Sergey Smolov
11
*Шаг 1*
12 22 Sergey Smolov
HDL-описание подается на вход парсеру, который выполняет лексический и синтаксический анализ и строит _граф потока управления_ (Control Flow Graph, CFG). Выражения парсер представляет в виде ориентированных ациклических графов, внутренние вершины которых помечены операциями, а конечные вершины - переменными или значениями. Вершины CFG принадлежат к следующим типам: начало (source), конец (sink), условный оператор (switch), ветвь условного оператора (case), ожидание (wait), порождение процессов (fork), завершение процессов (join), присваивание (assignment) и цикл (loop). Вызовы функций и процедур разворачиваются при трансляции в подграфы CFG.
13
14
*Шаг 2*
15
Каждой вершине CFG сопоставляется синтаксическое выражение, называемое _условием активации_ (activation node). Для вершин типа wait и source оно равно 1. Для прочих вершин оно вычисляется как сумма произведений условий активации родительских (parent) вершин на условия активации исходящих из них ребер. Условие активации ребра равно 1 для всех ребер, которые НЕ исходят из вершин fork, wait и source. В указанных случаях
16 19 Sergey Smolov
17 21 Sergey Smolov
h2. Cheng K., Krishnakumar A. 1996 Automatic generation of functional vectors using the extended finite state machine model
18 10 Sergey Smolov
19 7 Sergey Smolov
На вход алгоритму подается описание на языках VHDL или C (BESTMAP-C - см. Jou, J-Y., Rothweiler, S., Ernst, R., Sutarwala, S., and Prabhu, A. 1989. BESTMAP: Behavioral Synthesis from C. In International Workshop on Logic Synthesis (Research Triangle Park, NC, May).)
20 4 Sergey Smolov
21
*Шаг 1*
22 8 Sergey Smolov
Промежуточное представление кода строится с помощью Bridge AT & T Behaviour Synthesis System. По синхронной части кода (synchronous section) строится _дерево операторов_ (statement tree) _T_. Листовыми вершинами дерева являются базовые блоки (последовательности присваиваний). Ветви дерева снабжены атрибутами. Атрибуты - это выражения булева типа, соответствующие ветвям условных операторов в исходном коде. Не указано, каким образом выбираются переменные состояния (state variables), однако на *Шаге 3* они считаются уже определенными.
23 5 Sergey Smolov
24
*Шаг 2*
25 7 Sergey Smolov
Строится список всех возможных комбинаций условий на входные сигналы. Условия извлекаются из дерева операторов. Извлеченные комбинации проходят процедуру _ортогонализации_, такую, что каждая исходная комбинация оказывается представимой в виде суперпозиции нескольких ортогональных условий. В результате строится множество ортогонализованных условий _I_.
26 1 Sergey Smolov
27
*Шаг 3*
28 7 Sergey Smolov
Предыдущий шаг повторяется для всех условий, содержащих переменные состояния. В результате строится множество ортогонализованных условий _C_.
29
30
*Шаг 4*
31 11 Sergey Smolov
Собственно, построение EFSM по дереву T, и множествам C и I. Данный шаг в статье написан в весьма общем виде, псевдокод отсутствует. Результатом данного шага является _граф переходов между блоками_ (block transition graph), формальное определение которого в статье не приводится.
32 7 Sergey Smolov
33
*Шаг 5*
34 1 Sergey Smolov
Стабилизация графа переходов между блоками. Алгоритм стабилизации приводится в статье с использованием псевдокода. Идея алгоритма состоит в расщеплении слишком общих условий на более частные и не пересекающиеся, что позволяет исключить недетерминированные переходы в модели (Lee, D., Yannakakis, M. 1992. Online minimization of transition systems). Однако допускаются так называемые _частично стабильные переходы_ (semi-stable transitions). В таких переходах 1) действия (update functions) имеют вид x := x + c, где c - константа, а x - переменная состояния; 2) мощность множества конечных вершин равна 2; 3) одной из конечных вершин является начальная вершина, т.е. имеется цикл. В статье показывается, что для таких вершин в процессе обхода можно вычислить количество итераций, которое потребуется, чтобы выйти из цикла. Утверждается, что это допущение сокращает потребление вычислительных ресурсов (времени и памяти), по сравнению с алгоритмом _стабилизации_.
35 10 Sergey Smolov
36 21 Sergey Smolov
h2. Guglielmo G.D., Guglielmo L.D., Fummi F., Pravadelli G. 2011 Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs
37 12 Sergey Smolov
38
Целью метода является построение EFSM-моделей, которые легко обходить (easy-to-traverse). Обход EFSM-модели является основной техникой для генерации тестов.
39 13 Sergey Smolov
40
*Шаг 1*
41
Построение "эталонной" EFSM-модели (Reference EFSM, REFSM).
42 16 Sergey Smolov
На вход алгоритму подается HDL-описание в виде _конечного автомата с потоком данных_ (FSM with Datapath, FSMD). FSMD-модель - это комбинация FSM (control path) и _конвейера данных_ (data path). Как правило, FSM-компонент осуществляет прием входных сигналов, чтение переменных состояния и формирование запроса на обработку данных. Запрос передается конвейеру, который его выполняет и возвращает результат FSM-компоненту. FSMD-модель строится методом Giomi ( Giomi J. 1995 Finite state machine extraction from hardware description languages).
43 13 Sergey Smolov
44 1 Sergey Smolov
*Шаг 2*
45 14 Sergey Smolov
Построение "наибольшей" EFSM-модели (Largest EFSM, LEFSM). На данном шаге выполняется преобразование переходов REFSM, содержащих условные операторы, в переходы LEFSM, не содержащие таковых. Процесс завершается построением LEFSM, количество состояний в которой является наибольшим среди всех шагов алгоритма.
46
47
*Шаг 3*
48
Построение "наименьшей" EFSM-модели (Smallest EFSM, SEFSM). На данном шаге выполняется группировка совместимых переходов LEFSM. Процесс завершается построением SEFSM, количество состояний в которой является наименьшим среди всех шагов алгоритма.
49
50
*Шаг 4*
51
Дополнительные оптимизации, приводящие к построению "полу-стабилизированной" EFSM (Semi-Stabilized EFSM, (S^2)EFSM)