EFSM Building (Related Work)¶

Алгоритмы извлечения EFSM-моделей из исходного кода HDL-описаний. Все перечисленные методы строят по одному EFSM на каждый процесс целевого HDL-описания.

• Table of contents
• EFSM Building (Related Work)
  • Giomi J.-C. 1995 Finite State Machine Extraction From Hardware Description Languages
  • Cheng K., Krishnakumar A. 1996 Automatic generation of functional vectors using the extended finite state machine model
  • Guglielmo G.D., Guglielmo L.D., Fummi F., Pravadelli G. 2011 Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs

Giomi J.-C. 1995 Finite State Machine Extraction From Hardware Description Languages¶

Алгоритм строит FSM-модели - частный случай EFSM-моделей - по HDL-описанию. Метод применим только к описаниям, которые синхронизируются единственным clock. Кроме того, все wait-выражения в исходном коде также синхронизируются единственным clock.
Построенные FSM-модели предполагается использовать для синтеза netlist.

Шаг 1
HDL-описание подается на вход парсеру, который выполняет лексический и синтаксический анализ и строит граф потока управления (Control Flow Graph, CFG). Выражения парсер представляет в виде ориентированных ациклических графов, внутренние вершины которых помечены операциями, а конечные вершины - переменными или значениями. Вершины CFG принадлежат к следующим типам: начало (source), конец (sink), условный оператор (switch), ветвь условного оператора (case), ожидание (wait), порождение процессов (fork), завершение процессов (join), присваивание (assignment) и цикл (loop). Вызовы функций и процедур разворачиваются при трансляции в подграфы CFG. Для loop с фиксированным числом итераций предполагается использовать процедуру развертывания (unrolling).

Шаг 2
По CFG осуществляется поиск в глубину (depth-first search).
Каждой вершине 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 называется активируемым (activated path), если для каждого его ребра условие активации не принимает значение 0.

Шаг 3
Для каждой вершины CFG вычисляется набор выражений над данными (data expression) для всех переменных CFG. Выражения над данными имеют вид de_node(v) = val(v), где de_node(v) - обозначение для выражения для вершины node и переменнной v, val(v) - значение, определяемое типом вершины. В вершине source val(v) есть начальное значение v, в вершине wait - предыдущее значение v, в assignment - выражение, присваиваемое переменной, в прочих случаях - сумма выражений над данными для указанной переменной и всех родительских вершин, умноженных на условия активации родительских вершин.

Шаг 4
На данном шаге выполняется оптимизация выражений над данными, построенных на предыдущем шаге. Целью оптимизации является устранение ненужных условий.
Для заданной вершины n CFG-модели определяется множество неявных предыдущих состояний (Implicit Previous State, IPS) - множество wait-вершин, которые являются ближайшими к вершины n в направлении, противоположном потоку выполнения. Вершина s принадлежит IPS(n), если она принадлежит классу wait или source и между ней и n существует хотя бы один активируемый путь, не содержащих других вершин класса wait.
Вводится понятие максимального множества расширенного уровня (Extended Level Maximal Set, ELMS). Пусть необходимо оптимизировать выражение над данными для переменной v в вершине n.

Шаг 5
Определение начального состояния FSM. Одним из относительно простых способов является поиск кода (и состояния), который выполняется (и достигается) по reset. Сигнал reset задается пользователем.

Cheng K., Krishnakumar A. 1996 Automatic generation of functional vectors using the extended finite state machine model¶

На вход алгоритму подается описание на языках 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-модель предполагается использовать для генерации по ней тестов.

Шаг 1
Промежуточное представление кода строится с помощью Bridge AT & T Behaviour Synthesis System. По синхронной части кода (synchronous section) строится дерево операторов (statement tree) T. Листовыми вершинами дерева являются базовые блоки (последовательности присваиваний). Ветви дерева снабжены атрибутами. Атрибуты - это выражения булева типа, соответствующие ветвям условных операторов в исходном коде. Не указано, каким образом выбираются переменные состояния (state variables), однако на Шаге 3 они считаются уже определенными.

Шаг 2
Строится список всех возможных комбинаций условий на входные сигналы. Условия извлекаются из дерева операторов. Извлеченные комбинации проходят процедуру ортогонализации, такую, что каждая исходная комбинация оказывается представимой в виде суперпозиции нескольких ортогональных условий. В результате строится множество ортогонализованных условий I.

Шаг 3
Предыдущий шаг повторяется для всех условий, содержащих переменные состояния. В результате строится множество ортогонализованных условий C.

Шаг 4
Собственно, построение EFSM по дереву T, и множествам C и I. Данный шаг в статье написан в весьма общем виде, псевдокод отсутствует. Результатом данного шага является граф переходов между блоками (block transition graph), формальное определение которого в статье не приводится.

Шаг 5
Стабилизация графа переходов между блоками. Алгоритм стабилизации приводится в статье с использованием псевдокода. Идея алгоритма состоит в расщеплении слишком общих условий на более частные и не пересекающиеся, что позволяет исключить недетерминированные переходы в модели (Lee, D., Yannakakis, M. 1992. Online minimization of transition systems). Однако допускаются так называемые частично стабильные переходы (semi-stable transitions). В таких переходах 1) действия (update functions) имеют вид x := x + c, где c - константа, а x - переменная состояния; 2) мощность множества конечных вершин равна 2; 3) одной из конечных вершин является начальная вершина, т.е. имеется цикл. В статье показывается, что для таких вершин в процессе обхода можно вычислить количество итераций, которое потребуется, чтобы выйти из цикла. Утверждается, что это допущение сокращает потребление вычислительных ресурсов (времени и памяти), по сравнению с алгоритмом стабилизации.

Guglielmo G.D., Guglielmo L.D., Fummi F., Pravadelli G. 2011 Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs¶

Целью метода является построение EFSM-моделей, которые легко обходить (easy-to-traverse). Обход EFSM-модели является основной техникой для генерации тестов.

Шаг 1
Построение "эталонной" EFSM-модели (Reference EFSM, REFSM).
На вход алгоритму подается 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).

Шаг 2
Построение "наибольшей" EFSM-модели (Largest EFSM, LEFSM). На данном шаге выполняется преобразование переходов REFSM, содержащих условные операторы, в переходы LEFSM, не содержащие таковых. Процесс завершается построением LEFSM, количество состояний в которой является наибольшим среди всех шагов алгоритма.

Шаг 3
Построение "наименьшей" EFSM-модели (Smallest EFSM, SEFSM). На данном шаге выполняется группировка совместимых переходов LEFSM. Процесс завершается построением SEFSM, количество состояний в которой является наименьшим среди всех шагов алгоритма.

Шаг 4
Дополнительные оптимизации, приводящие к построению "полу-стабилизированной" EFSM (Semi-Stabilized EFSM, (S^2)EFSM)