Это доказательство команды, которое можно запустить в бесплатном хостинг-провайдере OnWorks с помощью одной из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
proof - Формальное доказательство между двумя поведенческими описаниями
СИНТАКСИС
доказательство [-a] [-d] file1 file2
ОПИСАНИЕ
Создан для работы с описанием потока данных, доказательство поддерживает то же подмножество VHDL, что и asimut
и бум и буг (для получения дополнительной информации об этом подмножестве, пожалуйста, позвоните в VHDL
руководство по эксплуатации). доказательство использует представление сокращенных упорядоченных двоичных диаграмм решений, которое позволяет
проектировщику легко доказать функциональную эквивалентность двух поведенческих
описания. доказательство обычно используется для сравнения поведенческой спецификации
с извлеченным поведением, полученным игл.
В режиме по умолчанию для описания выполняется этап сворачивания путем удаления всех
вспомогательные сигналы (BDD выходов, регистров и шин описаны с
входы или регистры). Два описания должны содержать одни и те же ресурсы.
(сигналы регистрируются с тем же именем). Можно использовать Inf. файл в игл (См.
дальнейшее замечание о ЯГЛЕ в этом документе), чтобы переименовать регистры в извлеченных
поведенческое описание (см. человек игл). Данные и команды (охраняемые
выражения) должны совпадать отдельно. Автобусы, соответствующие полностью заданному логическому
в обоих описаниях функции представлены логическим мультиплексором. Два
описания должны иметь один и тот же интерфейс (объект VHDL), в противном случае формальный доказательство
остановлен.
доказательство использует только две системные переменные среды, относящиеся к рабочему каталогу.
ОКРУЖАЮЩАЯ СРЕДА ПЕРЕМЕННЫЕ
MBK_WORK_LIB дает путь к поведенческим описаниям. Значение по умолчанию -
Текущий каталог.
MBK_CATA_LIB дает некоторые вспомогательные пути для поведенческих описаний. По умолчанию
значение - это текущий каталог.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
Параметры могут быть указаны в любом порядке перед именами файлов.
-a Эта опция спрашивает доказательство сохранить общие вспомогательные сигналы. доказательство сохраняет все
промежуточные сигналы, которые имеют одно и то же имя в обоих описаниях (общий сигнал
рассматривается как вход и выход каждого описания). Этот вариант может быть
полезно для описаний, содержащих большие уравнения. Может использоваться, когда доказательство и
не удалось или если вы хотите отладить в пошаговом режиме два разных описания.
-d Программа отображает ошибки, если описания поведения отличаются. Уравнения
отображаются, когда это возможно.
ПРИМЕР
доказательство -a -d сумматор1 сумматор2
ЯГЛЕ
YAGLE (Функциональная абстракция) теперь коммерчески распространяется компанией Avertec.
(http://www.avertec.com/). Более подробную информацию можно получить на их веб-сайте. Двоичные файлы
этого инструмента также можно загрузить для некоммерческих университетских исследований.
Используйте подтверждение онлайн с помощью сервисов onworks.net
