Основной доклад Intel о формальном расширении разума

Переиздано Платоном

Читают: 0

Компания Synopsys разместила на сайте SolvNet увлекательный доклад доктора Тео Дрейна из Intel Graphics. Тема — проверка эквивалентности пути к данным. Может показаться, что это еще одно официальное одобрение Synopsys VC, но вы все равно должны его посмотреть. Это расширяющее кругозор обсуждение использования и соображений в формальной форме, которое выведет вас за пределы рутинного руководства пользователя на более увлекательную территорию.

Основной доклад Intel о формальном

Интеллектуальное понимание против выборочного тестирования

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

Формальный побуждает вас понимать функциональность на глубоком уровне (по крайней мере, если вы хотите получить ценный результат). В приведенном выше примере простой вопрос — может ли z когда-либо состоять из единиц — не может продемонстрировать пример за миллиард циклов на симуляторе. Неудивительно, ведь это крайний случай. Формальный тест дает конкретный и очень неочевидный пример за 1 секунд и может доказать, что это единственный такой случай за чуть меньшее время.

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

Проблемы со спецификацией

Следующий пример Тео основан на автомате по продаже жуков (назван так потому, что при нажатии кнопки вы получаете жука). Это выглядит как довольно простая проблема проверки эквивалентности C и RTL, модель C слева, модель RTL справа. Одним из сюрпризов для Тео в первые годы его формальной работы было то, что поведение сдвига вправо в C-модели не полностью определено в стандарте C, даже несмотря на то, что gcc будет вести себя разумно. Однако DPV будет жаловаться на несоответствие в сравнении с RTL, как и должно быть. На неопределенное поведение опасно полагаться.

Формальный, как автомат по продаже жуков

Сравнение спецификаций между C и RTL сопряжено с другими опасностями, особенно в отношении разрядности. Усечение или потеря бита переноса в промежуточном сигнале (№ 3 выше) являются хорошими примерами. Это проблемы со спецификацией? Может быть, серая зона между спецификацией и вариантами реализации.

Помимо проверки эквивалентности

Основная цель DPV, по-видимому, состоит в том, чтобы проверить эквивалентность между ссылкой C или RTL и реализацией RTL. Но такая необходимость возникает относительно нечасто, и есть другие полезные способы применения такой технологии, пусть и немного нестандартные. Первая классика в мире реализации — я внес изменение, исправил ошибку — внес ли я какие-либо новые ошибки в результате? Немного похоже на проверку SEQ после добавления синхронизации. Анализ достижимости в выходных данных блока может быть еще одним полезным приложением в некоторых случаях.

Не только проверка эквивалентности

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

Заворачивать

Тео завершает обсуждением методологий, важных для производственного использования, ограничений, регрессий и сравнений с устаревшими моделями RTL. Кроме того, необходимо знать, действительно ли то, что вы проверяете, соответствует спецификации естественного языка верхнего уровня.

Очень бодрящая беседа, стоит посмотреть здесь, на Солвнете!

Поделитесь этим постом через: