Тестирование софта - статьи
ce076b8f

Сравнение с существующими подходами


В данном разделе приводится сравнение предлагаемого подхода с существующими методами спецификации аппаратуры, поддерживаемыми современными языками верификации аппаратуры (HVL, hardware verification languages). Языки верификации аппаратуры, к которым относятся PSL, OpenVera, SystemVerilog и др. [], включают в себя конструкции языков описания аппаратуры, языков программирования, а также специальные средства, ориентированные на разработку спецификаций и тестов. К последним относятся средства спецификации поведения, определения структуры тестового покрытия и генерации тестовых данных. Мы сравниваем только способы спецификации.

Средства спецификации поведения, используемые в современных языках верификации аппаратуры, базируются на темпоральной логике линейного времени (LTL, linear temporal logic) и/или темпоральной логике ветвящегося времени (CTL, computation tree logic) []. Языки, по крайней мере, по части спецификации, имеют следующие корни: ForSpec (Intel) [] (для языков, использующих логику LTL ) и Sugar (IBM) [] (для языков, использующих логику CTL). Ниже приведена диаграмма, показывающая влияние некоторых языков верификации аппаратуры друг на друга.

Логика CTL используется преимущественно для формальной верификации систем. Для целей симуляции и тестирования больший интерес представляет логика линейного времени LTL. Поскольку все языки верификации аппаратуры, в которых используется LTL, имеют схожие средства спецификации, для сравнения с предлагаемым подходом мы будем использовать только один из них - OpenVera []. Данный язык поддерживается многими инструментами; кроме того, он является открытым.

Рис. 5. Влияние языков верификации аппаратуры друг на друга.

Язык OpenVera был разработан в 1995 году компанией Systems Science. Первоначальное название языка - Vera. В 1998 году System Science была поглощена компанией Synopsys. В 2001 году Synopsys сделала язык открытым и переименовала его в OpenVera. Для спецификации поведения OpenVera предоставляет специальный язык формулирования темпоральных утверждений (temporal assertions), который называется OVA (OpenVera assertions) [, ].

OVA оперирует с ограниченными по времени последовательностями событий, в которых можно обращаться к прошлому и будущему.
Из простых последовательностей можно строить более сложные с помощью логических связок, таких как AND и OR, или используя регулярные выражения. В языке имеются средства объединения темпоральных утверждений в параметризованные библиотеки спецификаций. Проиллюстрируем синтаксис OVA на простом примере. // тактовый сигнал clock negedge(clk) { // граничные значения счетчика bool cnt_00: (cnt == 8'h00); bool cnt_ff: (cnt == 8'hff); // событие переполнения счетчика event e_overflow: cnt_ff #1 cnt_00; } // утверждение, запрещающее переполнение счетчика assert a_overflow: forbid(e_overflow); В примере определяется событие переполнения счетчика e_overflow, а утверждение a_overflow запрещает возникновение такого события. В подходе OpenVera, как и в других подходах на основе темпоральных логик, упор делается на временнýю декомпозицию операций. Для каждой операции сначала выделяется ее временнáя структура - допустимые последовательности событий и задержки между ними; затем определяются предикаты, описывающие отдельные события; после этого предикаты, относящиеся к одному моменту времени, некоторым образом группируются (Рис. 6).

Рис. 6. Построения спецификации в подходах на основе темпоральных логик. В подходе, предлагаемом нами, основной акцент ставится на функциональную декомпозицию операций. Первым делом выделяется функциональная структура операции - набор микроопераций; каждая микрооперация специфицируется; после этого производится временнáя композиция спецификаций (). Мы полагаем, что функциональная структура операции более устойчива по сравнению с временнóй. Тем самым, подходы, основанные на функциональной декомпозиции операций, позволяют разрабатывать спецификации, более устойчивые к изменениям реализации по сравнению с подходами на основе временнóй декомпозиции. К достоинствам предлагаемого подхода также можно отнести наглядность и простоту. Пред- и постусловия обычно понятнее формул темпоральной логики и не требуют от разработчика тестов каких-нибудь специальных знаний.

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