Неокончательное утверждение в Synopsys VC Formal

Question

2 вопроса -

1. В формальной проверке на основе утверждений, если я получу неокончательное утверждение, то каковы различные подходы для обработки этого утверждения или его слияния?
2. Правильный ли подход - разработать эталонный RTL и написать утверждения для сравнения выходных эталонных RTL с выходом DUT на каждом активном фронте тактового сигнала? Это увеличит действительные пространства состояний и, следовательно, сложность, время выполнения также?

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

Answer 1

У меня есть ответ на мой собственный вопрос, поэтому я здесь размещаю его.

Неокончательные утверждения являются естественной частью формальной проверки. Таким образом, отмена подтверждения все еще возможна, если у вас есть "Необходимая глубина доказательства". (Это похоже на покрытие в Проверке на основе моделирования, где вы все еще можете подписать подтверждение, если у вас есть необходимые номера покрытия). Чтобы получить "Необходимую глубину доказательства", необходимо связаться с командой разработчиков.

Глубина ограниченного доказательства> Требуемая глубина доказательства => Эквивалент полной проверки

Ограниченное доказательство может быть связано с несколькими причинами.

• Государственное пространство дизайна и / или утверждения
• Сложность дизайна и / или утверждения
• Параметры инструмента (алгоритм ограничения времени выполнения уровня усилия)

Поэтому ваш подход должен заключаться в том, чтобы получить "Необходимое доказательство".

Теперь, чтобы получить Requid Proof Bound, есть различные варианты.

• Параметры инструмента / ресурса (уровень усилия, время выполнения, ограничение памяти)
• Состояние пространства и сложности вариантов
  • Изменить / добавить ограничения
  • Blackboxing
  • Вырезать-очки
  • Изменить утверждения
  • Изменить значения параметров для параметризованных проектов
  • Состояние сброса на основе моделирования
  • Руководствуясь доказательства
  • Абстракции

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

Да, сравнение эталонной модели и выходных данных тестируемого устройства может увеличить сложность, поэтому при необходимости эталонная модель должна использоваться минимально.