Использование CTESK для спецификации аппаратуры

Инструмент разработки тестов CTESK предоставляет достаточно универсальные средства для спецификации систем с асинхронным интерфейсом []. Эти средства были адаптированы для спецификации модулей аппаратного обеспечения. Рассмотрим подробнее процесс разработки спецификаций.

Для каждой операции, реализуемой модулем, пишется спецификационная функция, в которой определяется предусловие операции и структура тестового покрытия. Постусловие спецификационной функции обычно возвращает true, поскольку все проверки, как правило, определяются в постусловиях микроопераций: // спецификация операции specification void operation_spec(...) { // предусловие операции pre { ... } // определение структуры тестового покрытия coverage C { ... } // постусловие операции обычно возвращает true post { return true; } }

Для каждой микрооперации, входящей в состав специфицируемой операции, пишется функция отложенной реакции, в которой определяется ее постусловие: // спецификация микрооперации reaction Operation* micro_return(void) { // постусловие микрооперации\ post { ... } }

Далее определяется функция временнóй композиции микроопераций, которая, во-первых, добавляет стимул (операцию вместе с набором аргументов) в очередь стимулов с указанием времени, необходимого для обработки стимула (time), во-вторых, для каждой микрооперации добавляет соответствующую реакцию в очередь реакций с указанием номера такта (относительно текущего времени), в конце которого следует осуществить проверку реакции (ticki): // временная композиция микроопераций void operation_time_comp(...) { Operation *descriptor = create_operation(...); // добавление стимула в очередь стимулов register_stimulus(create_stimulus(time, descriptor))); // добавление реакций в очередь реакций register_reaction(micro1_return, tick1, descriptor); ... register_reaction(micron_return, tickn, descriptor); }

Очередь стимулов содержит стимулы, обрабатываемые модулем в текущее время. Для каждого стимула в очереди хранится время, которое он уже обрабатывается.
Очередь реакций содержит еще не завершенные микрооперации. Для каждой микрооперации хранится время, через которое микрооперация завершится и можно будет осуществить проверку реакции. Изменение времени осуществляется функцией сдвига времени. После изменения времени вызываются функции обработки очередей стимулов и реакций. Функция обработки очереди стимулов удаляет из очереди полностью обработанные стимулы. Функция обработки очереди реакций регистрирует отложенные реакции для всех завершившихся микроопераций, которые после этого удаляются из очереди. Для иллюстрации синтаксиса языка SeC приведем очень простой пример. Рассмотрим устройство, называемое 8-ми битным счетчиком (Рис. 4).

Рис. 4.Схема входов и выходов 8-ми битного счетчика. Интерфейс счетчика состоит из двух двоичных входов clk и rst и одного 8-ми битного выходного регистра cnt. Если уровень сигнала rst низкий, фронт сигнала тактового импульса clk увеличивает счетчик cnt по модулю 256; иначе счетчику присваивается значение 0. Ниже приводится спецификационная функция, описывающая операцию увеличения счетчика, то есть поведение счетчика в ответ на фронт clk при низком уровне сигнала rst. Поскольку операция является простой, спецификация выполнена без привлечения функций отложенных реакций. // спецификация операции увеличения счетчика specification void increment_spec(counter_8bit *counter) updates cnt = counter->cnt, rst = counter->rst { // предусловие операции pre { return rst == false; } // определение структуры тестового покрытия coverage C { return { SingleBranch, "Single branch" }; } // постусловие операции post { return cnt == (@cnt + 1) % 0xff; } }

Содержание раздела

---

Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий

---