Общеизвестно, что слабым звеном в технологической цепочке проектирования сложного аппаратного обеспечения является функциональная верификация. Согласно Бергерону (Janiсk Bergeron) [1] функциональная верификация занимает около 70% общего объема трудозатрат, число инженеров, занимающихся верификацией, примерно вдвое превосходит число проектировщиков, а размер исходного кода тестов (testbenches) достигает 80% общего размера кода проекта.
Принцип функционального тестирования
Для того, чтобы граф состояний конечного автомата был сильно связен, необходимо чтобы для каждого события, используемого в тестовых воздействиях, существовало тестовое воздействие с обратным событием, так как в противном случае образуются тупиковые состояния теста...[2][3] Теория конечных автоматов является только одним из примеров достойного применения математического формализма в обширной области моделирования:
Функциональная декомпозиция или временная декомпозиция - Выбор за вами…
Средства спецификации поведения, используемые в современных языках верификации аппаратуры, базируются на темпоральной логике линейного времени (LTL, linear temporal logic) и/или темпоральной логике ветвящегося времени (CTL, computation tree logic). Языки по части спецификации имеют следующие корни: ForSpec (Intel) (для языков, использующих логику LTL) и Sugar (IBM) (для языков, использующих логику CTL). Ниже приведена диаграмма, показывающая влияние некоторых языков верификации аппаратуры друг на друга:
Логика CTL используется преимущественно для формальной верификации систем. Для целей симуляции и тестирования больший интерес представляет логика линейного времени LTL. Поскольку все языки верификации аппаратуры, в которых используется LTL, имеют схожие средства спецификации, для дальнейшего описания мы будем использовать только один из них - OpenVera. Данный язык поддерживается многими инструментами и он является открытым. Язык OpenVera был разработан в 1995 году компанией Systems Science. Первоначальное название языка - Vera. В 1998 году System Science была поглощена компанией Synopsys. В 2001 году Synopsys сделала язык открытым и переименовала его в OpenVera. Для спецификации поведения OpenVera предоставляет специальный язык формулирования темпоральных утверждений (temporal assertions), который называется OVA (OpenVera assertions). В подходе OpenVera, как и в других подходах на основе темпоральных логик, упор делается на временнýю декомпозицию операций. Дальнейшее развитие этого направления привело к появлению стандартов IEEE 1364 и IEEE 1800
Технология тестирования UniTesK была разработана в Институте системного программирования РАН. Первоначальное и основное назначение технологии — разработка качественных функциональных тестов для программного обеспечения, но современная область применения технологии UniTesK гораздо шире — функциональное тестирование моделей программного и аппаратного обеспечения. Технология UniTesK была разработана на основе опыта, полученного при разработке и применении технологии KVEST[3] (kernel verification and specification technology). Общими чертами этих технологий являются использование формальных спецификаций в форме пред- и постусловий интерфейсных операций и инвариантов типов данных для автоматической генерации оракулов (компонентов тестовой системы, осуществляющих проверку правильности поведения целевой системы), а также применение конечно-автоматных моделей для построения последовательностей тестовых воздействий. В отличие от технологии KVEST, в которой для спецификации требований использовался язык RSL (RAISE specification language[4]) , технология UniTesK использует расширения широко известных языков программирования. На данный момент разработаны инструменты, поддерживающие работу с расширениями языков C, Java и C#: CTesK , J@T и Ch@se, соответственно.
[3]. I. Bourdonov, A. Kossatchev, A. Petrenko, and D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. FM99: Formal Methods. LNCS 1708, Springer-Verlag, 1999, pp. 608-621.
[4]. The RAISE Language Group. The RAISE Specification Language. Prentice-Hall BCS Practitioner Series. Prentice-Hall, Inc., 1993.
