EFSM Building (Related Work) » History » Version 29
Sergey Smolov, 03/30/2017 11:54 AM
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 | 25 | Sergey Smolov | Алгоритм строит FSM-модели - частный случай EFSM-моделей - по HDL-описанию. Метод применим только к описаниям, которые синхронизируются единственным clock. Кроме того, все wait-выражения в исходном коде также синхронизируются единственным clock. |
10 | 26 | Sergey Smolov | Построенные FSM-модели предполагается использовать для синтеза netlist. |
11 | 1 | Sergey Smolov | |
12 | *Шаг 1* |
||
13 | 29 | Sergey Smolov | HDL-описание подается на вход парсеру, который выполняет лексический и синтаксический анализ и строит _граф потока управления_ (Control Flow Graph, CFG). Выражения парсер представляет в виде ориентированных ациклических графов, внутренние вершины которых помечены операциями, а конечные вершины - переменными или значениями. Вершины CFG принадлежат к следующим типам: начало (source), конец (sink), условный оператор (switch), ветвь условного оператора (case), ожидание (wait), порождение процессов (fork), завершение процессов (join), присваивание (assignment) и цикл (loop). Вызовы функций и процедур разворачиваются при трансляции в подграфы CFG. |
14 | 22 | Sergey Smolov | |
15 | *Шаг 2* |
||
16 | 1 | Sergey Smolov | По CFG осуществляется поиск в глубину (depth-first search). |
17 | 29 | Sergey Smolov | Каждой вершине CFG сопоставляется синтаксическое выражение, называемое _условием активации_ (activation node). Для вершин типа wait и source оно равно 1. Для прочих вершин оно вычисляется как сумма произведений условий активации родительских (parent) вершин на условия активации исходящих из них ребер. Условие активации ребра равно 1 для всех ребер, которые НЕ исходят из вершин fork, wait, switch и source. Для ребер, исходящих из вершин типа source и fork, условия активации имеют вид равенства @ISR == val_w@, где ISR - неявная переменная состояния (Implicit State Register). Для ребра, исходящего из вершины типа fork условие активации формулируется как предикат, равный 1 для текущей ветви и 0 для всех остальных ветвей, исходящих из той же вершины. Для ребра, исходящего из вершины типа switch условие строится в виде равенства @cond == val@, где cond - условие в узле switch, val - значение в узле case. Путь в CFG называется _активированным_, если для каждого его ребра условие активации не принимает значение 0. |
18 | |||
19 | *Шаг 3* |
||
20 | Для каждой вершины CFG вычисляется набор _выражений над данными_ (data expression) для всех переменных CFG. Выражения над данными имеют вид равенств @de_node(v) == val(v)@, где @de_node(v)@ - обозначение для выражения для вершины @node@ и переменнной @v@, @val(v)@ - значение, определяемое типом вершины. В вершине source @val(v)@ есть начальное значение @v@, в вершине wait - |
||
21 | 19 | Sergey Smolov | |
22 | 21 | Sergey Smolov | h2. Cheng K., Krishnakumar A. 1996 Automatic generation of functional vectors using the extended finite state machine model |
23 | 10 | Sergey Smolov | |
24 | 27 | 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).). Построенную EFSM-модель предполагается использовать для генерации по ней тестов. |
25 | 4 | Sergey Smolov | |
26 | *Шаг 1* |
||
27 | 8 | Sergey Smolov | Промежуточное представление кода строится с помощью Bridge AT & T Behaviour Synthesis System. По синхронной части кода (synchronous section) строится _дерево операторов_ (statement tree) _T_. Листовыми вершинами дерева являются базовые блоки (последовательности присваиваний). Ветви дерева снабжены атрибутами. Атрибуты - это выражения булева типа, соответствующие ветвям условных операторов в исходном коде. Не указано, каким образом выбираются переменные состояния (state variables), однако на *Шаге 3* они считаются уже определенными. |
28 | 5 | Sergey Smolov | |
29 | *Шаг 2* |
||
30 | 7 | Sergey Smolov | Строится список всех возможных комбинаций условий на входные сигналы. Условия извлекаются из дерева операторов. Извлеченные комбинации проходят процедуру _ортогонализации_, такую, что каждая исходная комбинация оказывается представимой в виде суперпозиции нескольких ортогональных условий. В результате строится множество ортогонализованных условий _I_. |
31 | 1 | Sergey Smolov | |
32 | *Шаг 3* |
||
33 | 7 | Sergey Smolov | Предыдущий шаг повторяется для всех условий, содержащих переменные состояния. В результате строится множество ортогонализованных условий _C_. |
34 | |||
35 | *Шаг 4* |
||
36 | 11 | Sergey Smolov | Собственно, построение EFSM по дереву T, и множествам C и I. Данный шаг в статье написан в весьма общем виде, псевдокод отсутствует. Результатом данного шага является _граф переходов между блоками_ (block transition graph), формальное определение которого в статье не приводится. |
37 | 7 | Sergey Smolov | |
38 | *Шаг 5* |
||
39 | 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) одной из конечных вершин является начальная вершина, т.е. имеется цикл. В статье показывается, что для таких вершин в процессе обхода можно вычислить количество итераций, которое потребуется, чтобы выйти из цикла. Утверждается, что это допущение сокращает потребление вычислительных ресурсов (времени и памяти), по сравнению с алгоритмом _стабилизации_. |
40 | 10 | Sergey Smolov | |
41 | 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 |
42 | 12 | Sergey Smolov | |
43 | Целью метода является построение EFSM-моделей, которые легко обходить (easy-to-traverse). Обход EFSM-модели является основной техникой для генерации тестов. |
||
44 | 13 | Sergey Smolov | |
45 | *Шаг 1* |
||
46 | Построение "эталонной" EFSM-модели (Reference EFSM, REFSM). |
||
47 | 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). |
48 | 13 | Sergey Smolov | |
49 | 1 | Sergey Smolov | *Шаг 2* |
50 | 14 | Sergey Smolov | Построение "наибольшей" EFSM-модели (Largest EFSM, LEFSM). На данном шаге выполняется преобразование переходов REFSM, содержащих условные операторы, в переходы LEFSM, не содержащие таковых. Процесс завершается построением LEFSM, количество состояний в которой является наибольшим среди всех шагов алгоритма. |
51 | |||
52 | *Шаг 3* |
||
53 | Построение "наименьшей" EFSM-модели (Smallest EFSM, SEFSM). На данном шаге выполняется группировка совместимых переходов LEFSM. Процесс завершается построением SEFSM, количество состояний в которой является наименьшим среди всех шагов алгоритма. |
||
54 | |||
55 | *Шаг 4* |
||
56 | Дополнительные оптимизации, приводящие к построению "полу-стабилизированной" EFSM (Semi-Stabilized EFSM, (S^2)EFSM) |