Project

General

Profile

EFSM Building (Related Work) » History » Revision 14

Revision 13 (Sergey Smolov, 03/28/2017 03:14 PM) → Revision 14/40 (Sergey Smolov, 03/28/2017 04:18 PM)

h1. EFSM Building (Related Work) 

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

 {{toc}} 

 h2. 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).) 

 *Шаг 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. 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). 

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

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

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