Использование 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).
