Сравнение с существующими подходами
В данном разделе приводится сравнение предлагаемого подхода с существующими методами спецификации аппаратуры, поддерживаемыми современными языками верификации аппаратуры (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).
