Retrascope

h1. EFSM Building (Related Work)

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

{{toc}}

h2. 1995 Giomi J.-C. 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 осуществляется поиск в ширину (bredth-first search). Фактически, в время выполнения поиска в ширину осуществляется и Шаг 3.

Каждой вершине 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*

На данном шаге выполняется оптимизация выражений над данными, построенных на предыдущем шаге. Целью оптимизации является устранение ненужных условий.

По CFG осуществляется поиск в глубину (depth-first search).

Для заданной вершины @n@ CFG-модели определяется множество _неявных предыдущих состояний_ (Implicit Previous State, IPS) - множество wait-вершин, которые являются ближайшими к вершины @n@ в направлении, противоположном потоку выполнения. Вершина @s@ принадлежит @IPS(n)@, если она принадлежит классу wait или source и между ней и @n@ существует хотя бы один активируемый путь, не содержащих других вершин класса wait.

Вводится понятие _максимального множества расширенного уровня_ (Extended Level Maximal Set, ELMS). Пусть необходимо оптимизировать выражение над данными для переменной @v@ в вершине @n@. Тогда @ELMS(n.v)@ - это множество наиболее отдаленных предков вершины @n@, таких, что каждый путь от них до @n@ является активируемым и не содержит вершин wait и присваиваний @v@. В таком случае выражение над данными @de_n(v)@ можно представить в виде суммы произведений (см. Шаг 3) для всех вершин из @ELMS(n,v)@.

Для каждого неявного состояния, сопоставленного вершине wait, вычисляются условия на переходы и выходные значения. Так, условие на переход по wait-вершине @i@ из @IPS(w)@ в wait-вершину @w@ вычисляется как сумма произведений условий активации вершин на условия активации исходящих из них ребер, соединяющих эти вершины с @w@ для всех родительских вершин для вершины @w@. Выходное значение для переменной @v@ вычисляется как сумма произведений условий активации вершин на выражения над данными для переменной @v@ в этих вершинах, для всех вершин из множества @ELMS(w, v)@.

*Шаг 5* 

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

*Шаг 6*

Неявные переменные состояния заменяются на _явные переменные состояния_ (Explicit State Register, ESR). Для каждой пары явных состояний определяются условия на переходы и выражения над данными для выходных переменных.

h2. 1996 Cheng K., Krishnakumar A. 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) одной из конечных вершин является начальная вершина, т.е. имеется цикл. В статье показывается, что для таких вершин в процессе обхода можно вычислить количество итераций, которое потребуется, чтобы выйти из цикла. Утверждается, что это допущение сокращает потребление вычислительных ресурсов (времени и памяти), по сравнению с алгоритмом _стабилизации_.

h2. 2006 Gilford M.E.J., Walker G.N., Tredinnick J.L., Dane M.W.P., Reynolds M.J.. Recognition of a State Machine in High-Level Integrated Circuit Description Language Code

Данный метод позволяет анализировать HDL-описания на языках VHDL и Verilog и распознавать в них автоматные модели. Автоматные модели предоставляются

*Шаг 1* Идентифицировать все процессы

Процессы в HDL-описаниях идентифицируются по ключевым словам: @process@ для VHDL, @always@ и @initial@ для Verilog.

*Шаг 2* Идентифицировать синхронизуемые (clocked) процессы

Неформально, среди процессов выполняется поиск тех, которые содержат условные операторы, зависящие от синхросигнала, и меняющие состояние.

Формально, выполняется поиск процессов, имеющих нетривиальный список чувствительности и хотя бы один условный оператор @if@. Предполагается, что @if@ верхнего уровня содержит условия на переменные синхроимпульса @clock@ и сброса @reset@. Если условный оператор имеет ветви типа @else@ или @elseif@, то @reset@-выражение извлекается из ветви @if@, а @clock@-выражение - из ветвей @else@ или @elseif@. Если таких ветвей нет, то @clock@-выражение извлекается из ветви @if@. @reset@-выражение должно иметь вид (не)равенства, в одной части которого находится константа (или значение перечислимого типа), а в другой - переменная, которая в дальнейшем интерпретируется как @reset@. Если переменная @reset@ определена, то выполняется поиск @state@-переменной в наборе операторов присваивания, соответствующих @reset@-выражению в условном операторе. @clock@-выражение должно иметь вид либо функции одной переменной, либо предиката, состоящего из событийной части (event) и логической части (равенства в духе @reset@-выражения). Если переменная @clock@ определена, то выполняется поиск @state@-переменной в наборе присваиваний (или операторе @case@) из соответствующей ветви условного оператора.

*Шаг 3* Идентифицировать процессы переходов (transition)

Неформально, процессы переходов содержат присваивания, определяющие переменные состояния.

На множестве синхронизируемых процессов выполняется поиск таких процессов, что для каждого из них найдется хотя бы один процесс, в котором определяется переменная из данного процесса. Тогда процесс помечается как процесс перехода.

*Шаг 4* Идентифицировать выходные (output) процессы

Неформально, выходные процессы содержат присваивания значений выходным сигналам, не являющимся переменными состояния.

На множестве синхронизируемых процессов выполняется поиск таких процессов, что в каждом из них определяется хотя бы одна выходная переменная. Тогда процесс помечается как выходной.

*Шаг 5* Построить автоматную модель

Выполняется перебор всех процессов HDL-описания. Если для текущей переменной текущий процесс её использует, то сохраняются найденные в нем информация о @clock@ (название и тип фронта) и @reset@. По переменным процесса выполняется поиск @state@-переменной и @next state@-переменной. Ограничение алгоритма состоит в том, что эти переменные должны иметь одинаковый тип. Если процесс является первым, в котором @state@-переменной присваивается значение @next state@-переменной, то он помечается как @clocked@-процесс для данной @state@-переменной. Если процесс является первым процессом перехода для данной @state@-переменной, или первым процессом перехода, не являющимся синхронизуемым, то он помечается как @transition@-процесс для данной @state@-переменной. Если процесс является первым выходным процессом для данной @state@-переменной, или первым выходным процессом, не являющимся синхронизуемым изи процессом перехода, то он помечается как @output@-процесс для данной @state@-переменной.

Отметим, что результатом работы данного алгоритма является не оплноценная автоматная модель, а набор сведений о ней, таких как: название сигнала @clock@; название сигнала @reset@; название сигнала @state@; список состояний (значений, принимаемых переменной @state@); количество переходов модели (количество @transition@-процессов); количество выходов (@output@-процессов) и входов (@clocked@-процессов).

h2. 2011 Guglielmo G.D., Guglielmo L.D., Fummi F., Pravadelli G. 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).

ВАЖНО: в статье Giomi термин FSMD в явном виде не присутствует и не совсем понятно, что он делает здесь. HDL-описание, обрабатываемое методом Giomi, имеет некоторые синтаксические ограничения, но они напрямую не связаны с FSMD-представлением.

*Шаг 2*

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

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

рекурсивным образом выполняется расщепление на переходы, не содержащие условных операторов. Расщепление сопровождается созданием новых символических состояний LEFSM-модели. Часть перехода, являющаяся условным оператором, расщепляется на количество переходов, равное количеству ветвей в условном операторе. Для каждого "нового" перехода создается новое конечное состояние.

*Шаг 3*

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

Основная цель данного шага - обеспечить построение модели, которая была бы эквивалентна исходному HDL-описанию в смысле исполнения тестов. По-видимому, неявно предполагается, что за один такт EFSM-модель исполняет ровно один переход.

Шаг 3 включает в себя следующие операции:

# композиция совместимых переходов;

# устранение несовместимости переходов;

Пусть @tij@ из состояния @Si@ в состояние @Sj@ с охранным условием @eij@ и действием @uij@, а переход @tjk@ из состояния @Sj@ в @Sk@ с охранным условием @ejk@ и действием @ujk@. Говорят, что @tij@ _совместим_ с @tjk@, если @eij@ и @ejk@ могут быть истинны одновременно, и @uij@ не содержит присваиваний переменным, используемым в @ejk@. В таком случае переход @tij@ объединяют с переходом @tjk@: последний получает охранное условие @eij AND ejk@ и действие @uij OR ujk@.

Если переходы @tij@ и @tjk@ не являются совместимыми, то это может произойти по двум причинам:

* Если их охранные условия не могут быть одновременно истинными - в случае, если переходы являются вложенными (nested, соответствуют вложенным условным операторам), то это сигнализирует об ошибке в HDL-описании; если нет, то должна проводиться композиция с другими переходами, являющимися совместимыми;

* Если действие перехода @tij@ определяет переменную(ые), которые используются в охранному условии @tjk@ - в таком случае предлагается модифицировать код HDL-описания таким образом, чтобы для каждой переменной @v@ её значение менялось после проверок этого значения.

*Шаг 4*

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

Восстановление оригинальных состояний делается методом _стабилизации_ Cheng, Krishnakumar. Стабилизация проводится по некоторым переменным (не всем), чтобы избежать комбинаторного взрыва состояний и одновременно удалить часть условий, зависящих от внутренних переменных, из охранных условий переходов. Можно предположить, что, в первую очередь, стабилизация нацеливается на такие переменные, которые используются во всех охранных условиях  и всех действиях переходов SEFSM.