Современный мир не мыслим без
Современный мир не мыслим без огромного разнообразия электронных устройств. Мобильные телефоны, цифровые фотокамеры и переносные компьютеры давно стали неотъемлемыми атрибутами жизни человека. Специальные устройства управляют работой бытовой техники, контролируют бортовые системы самолетов и космических спутников, управляют медицинскими системами жизнеобеспечения. В основе практически всех этих систем лежит полупроводниковая аппаратура - кристаллы интегральных схем, состоящие из миллионов связанных друг с другом микроскопических транзисторов, которые, пропуская через себя электрические токи, реализуют требуемые функции. Чтобы убедиться, что аппаратура работает правильно, то есть реализует именно те функции, которые от нее ожидают пользователи, на практике используют функциональное тестирование. Требования, предъявляемые к качеству тестирования аппаратного обеспечения, очень высоки. Это связано не только с тем, что аппаратура лежит в основе всех информационных и управляющих вычислительных систем, в том числе достаточно критичных к сбоям и ошибкам. Большое влияние на формирование высоких требований оказывают также экономические факторы. В отличие от программного обеспечения, в котором исправление ошибки стоит сравнительно дешево, ошибка в аппаратном обеспечении, обнаруженная несвоевременно, может потребовать перевыпуск и замену продукции, а это сопряжено с очень высокими затратами. Так, известная ошибка в реализации инструкции FDIV микропроцессора Pentium [], заключающаяся в неправильном делении некоторых чисел с плавающей точкой, обошлась компании Intel в 475 миллионов долларов [, ]. С другой стороны, требования к срокам тестирования также очень высоки. Важно не затягивать процесс и выпустить продукт на рынок своевременно, пока он не потерял актуальность, и на него существует спрос. Как разработать качественный продукт своевременно, используя ограниченные ресурсы? В настоящее время для проектирования аппаратного обеспечения используются языки моделирования высокого уровня, которые позволяют значительно ускорить процесс разработки за счет автоматической трансляции описания аппаратуры на уровне регистровых передач (RTL, register transfer level) в описание аппаратуры на уровне логических вентилей (gate level).
Такие языки называются языками описания аппаратуры (HDL, hardware description languages), а модели, построенные на их основе - HDL-моделями или RTL-моделями . Языки описания аппаратуры позволяют значительно повысить продуктивность разработки аппаратного обеспечения, но они не страхуют от всех ошибок, поэтому функциональное тестирование по-прежнему остается актуальной и востребованной задачей. При современной сложности аппаратного обеспечения невозможно разработать приемлемый набор тестов вручную за разумное время. Необходимы технологии автоматизированной разработки тестов. В настоящее время разработка таких технологий и поддерживающих их инструментов выделилась в отдельную ветвь автоматизации проектирования электроники (EDA, electronic design automation) - автоматизацию тестирования (testbench automation). Основной задачей тестирования является проверка соответствия поведения системы предъявляемым к ней требованиям. Для возможности автоматизации такой проверки требования к системе должны быть представлены в форме, допускающей автоматическую обработку. Такую форму представления требований называют формальными спецификациями или просто спецификациями. В работе рассматривается определенный вид спецификаций - контрактные спецификации (contract specifications). Контрактные спецификации и процесс проектирования на их основе (DbC, Design-by-Contract) были введены Бертраном Майером (Bertrand Meyer) в 1986 году в контексте разработки программного обеспечения [, ]. Центральная метафора подхода заимствована из бизнеса. Компоненты системы взаимодействуют друг с другом на основе взаимных обязательств (obligations) и выгод (benefits). Если компонент предоставляет окружению некоторую функциональность, он может наложить предусловие (precondition) на ее использование, которое определяет обязательство для клиентских компонентов и выгоду для него. Компонент также может гарантировать выполнение некоторого действия с помощью постусловия (postcondition), которое определяет обязательство для него и выгоду для клиентских компонентов. Почему в своих исследованиях мы выбрали именно контрактные спецификации? Контрактные спецификации, с одной стороны, достаточно удобны для разработчиков, поскольку хорошо привязываются к архитектуре системы, с другой стороны, в силу своего представления стимулируют усилия по созданию независимых от реализации критериев корректности целевой системы [].Основное же их преимущество состоит в том, что они позволяют автоматически строить тестовые оракулы, проверяющие соответствие поведения целевой системы требованиям, описанным в спецификациях. Несколько слов о том, как организована статья. Во втором, следующем за введением, разделе даются общие сведения о моделях аппаратного обеспечения и типичной организации аппаратуры. В третьем разделе описывается предлагаемый подход к спецификации и проверке требований к аппаратному обеспечению. Четвертый раздел содержит краткий обзор технологии тестирования UniTESK и инструмента разработки тестов CTESK. В нем также описан способ использования инструмента для спецификации аппаратуры. В пятом разделе приводится сравнение предлагаемого подхода с существующими методами спецификации аппаратного обеспечения. Шестой раздел описывает опыт практического применения подхода. Наконец, в последнем, седьмом разделе делается заключение и очерчиваются направления дальнейших исследований.
