3. Функциональная верификация

Каждый компонент (транзистор, логический элемент или функциональный блок) схемы можно описать по его поведению как функцию входов и внут­реннего состояния. Объединяя описания этих элементов, можно сгенериро­вать модель всей схемы, в символической форме описывающей поведение рассматриваемой структуры. При формальной верификации данное расчет­ное поведение сравнивается с исходной спецификацией разработчика. Хо­тя два данных описания и не идентичны, они должны быть математиче­ски эквивалентными.

Формальная верификация — это предел мечтаний разработчика, кото­рого он желает добиться от средств автоматизированного проектирования: доказательство, что схема будет работать именно так, как задано. К со­жалению, до настоящего момента не было создано ни одного универсально­го средства верификации, которое получило бы широкое распространение. Сложность данной проблемы иллюстрируется следующим аргументом: что­бы доказать, что два описания схемы идентичны, необходимо сравнить их выходы для всех возможных входных последовательностей сигналов. Пробле­ма в том, что время требуемых для этого расчетов экспоненциально растет в зависимости от числа входов и состояний.

Тем не менее, сказанное не означает, что формальная верификация от­носится к области фантазий. Для определенных классов схем соответствую­щие принципы верификации были предложены и успешно реализованы. На­пример, существенно сузить пространство поиска позволяет предположение о синхронности схемы. Одним из основных направлений исследований явля­ется доказательство эквивалентности между конечными автоматами; опре­деленный прогресс в данной сфере уже наблюдается. В общем, формальная верификация делится на два основных класса.

• Доказательство эквивалентности. Проектирование часто следует по пу­ти уточнения, когда исходное высокоуровневое описание последовательно уточняется до более подробного. Средства доказательства эквивалентно­сти позволяют гарантировать, что получаемый результат функционально эквивалентен первоначальному описанию. Например, подобное средство может установить, что транзисторная схема статического КМОП-элемента НЕ-И с N входами действительно реализует задуманную функцию НЕ-И.

• Доказательство свойств. Разработчику часто нужно знать, сохраняют­ся ли в процессе проектирования некоторые заданные свойства. Возмож­но, к разработке применяется следующее требование: "В схеме никогда не должны возникать состязания". Добиться поставленной цели можно с по­мощью хорошего средства доказательства свойств; кроме того, средство может сообщить, почему условие не удовлетворяется.

Одним из необходимых условий реализации формальной верификации яв­ляется описание проекта, не допускающее неоднозначности и имеющее четко определенное значение (или семантику). При выполнении этого условия тех­ника формальной верификации весьма эффективна и полезна. Например, областью, в которой формальная верификация достигла существенных успе­хов, являются конечные автоматы (Finite State Machine — FSM). Секрет этих успехов кроется в хорошо определенной математической модели описания.

Хотя функциональная верификация еще не получила должного признания в сфере автоматизированного проектирования, она может стать одним из наиболее важных инструментов в арсенале разработчика цифровых систем. Чтобы этот прогноз подтвердился, необходима большая работа в сфере спе­цификации и интерпретации проектов.