FormalPro

Приложение FormalPro предназначено для контроля функциональной эквивалентности между разными уровнями реализации проекта ASIC или FPGA. Анализ эквивалентности выполняется методом формальной верификации тестируемого объекта с его референсным описанием и осуществляется на несколько порядков быстрее, чем поведенческое моделирование (часы и даже минуты вместо недель и дней). Основное назначение – сравнение эквивалентности вентильного уровня проекта на разных уровнях его реализации (от синтеза до tapeout) c исходным RTL описанием.

Основные преимущества

- Значительно сокращает время верификации

- Сравнивает функциональную эквивалентность двух уровней реализации проекта:

         - исходного RTL описания и вентильного описания после синтеза или внесения изменений

         - двух вентильных описаний после очередной итерации получения топологии проекта

         - двух RTL описаний при конверсии проекта из одного языка в другой

- Поддерживает проекты большой емкости:

         - Несколько миллионов вентилей

         - Весь кристалл целиком

- Обеспечивает быстрый процесс отладки:

         - Быстрое обнаружение и локализация расхождений

         - Быстрое повторное тестирование после устранения расхождений в одной сессии верификации

- Поддерживает FPGA

         - Xilinx, Altera, Actel

         - Автоматическая генерация файлов FVI и VIF

         - Ускорение процесса верификации

- Предоставляет удобный пользовательский интерфейс для ввода и настройки исходных описаний

- Обеспечивает возможность управления регрессионной верификацией в командном режиме

- Поддерживает языковые ограничения и TCL скрипты

- Обеспечивает инкрементную верификацию

         - Рекомпиляция только той части проекта, которая подверглась изменениям

         - Рестарт анализа с промежуточных точек