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

2 вопроса -

  1. В формальной проверке на основе утверждений, если я получаю неубедительное утверждение, то каковы различные подходы к обработке этого утверждения или его сведению?
  2. Является ли правильным подходом разработать эталонный rtl и написать утверждения для сравнения выходного сигнала эталонного rtl с выходным сигналом тестируемого устройства на каждом активном фронте тактового сигнала? Увеличит ли это действительные пространства состояний и, следовательно, сложность, а также время выполнения?

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


formal-verification synopsys-vcs
person Karan Shah    schedule 19.12.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

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

Ограниченная глубина цветопробы > Требуемая глубина цветопробы => Эквивалент полной пробы

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

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

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

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

  • Параметры инструмента/ресурса (уровень усилий, время выполнения, ограничение памяти)
  • State Space & Complexity Options
    • Modify/Add Constraints
    • Блэкбоксинг
    • Разрезы
    • Изменить утверждения
    • Изменить значения параметров для параметризованных проектов
    • Состояние сброса на основе моделирования
    • Управляемые доказательства
    • Абстракции

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

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

person Karan Shah    schedule 05.02.2016