как написать формальный тест восстановления сброса, который имеет длительное время

Я использовал для проверки модуля, состоящего из последовательного порта с набором регистров, с помощью динамических тестов. Один из тестов - это тест восстановления и сброса. Последовательность синхронизации: (i) записать случайные данные в регистр из последовательного порта (потребовалось 40 тактовых циклов) (ii) сбросить этот регистр и освободить его (iii) прочитать этот регистр из последовательного порта (потребовалось еще 40 тактовых циклов)

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

Более того, общий формальный тест сброса прост, он занимает всего 1 цикл, формальный инструмент начинает исследовать состояния пространства из состояния сброса. Но теперь я пытаюсь написать тест, в котором говорится, что после того, как DUT что-то сделало, поместите регистр в сброс, прочтите его, значение по-прежнему является значением сброса.


verilog system-verilog formal-verification formal-languages asic
person TyL    schedule 11.01.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вероятно, ваша проблема заключается в том, что инструмент изучает все возможные состояния, в которых он может применить сброс. То есть, если я загружаю регистр A значением 4, а регистр B загружаю 8 и применяю сброс, что произойдет. Теперь попробуйте, что регистр A равен 5, а регистр B равен 8, и я применяю сброс, что происходит. Теперь попробуйте, что регистр A равен 6, и ... вы поняли идею.

Вы можете написать эти тесты, но вам нужно сделать несколько вещей:

  • Не делайте сброса на старте. Таким образом, все регистры не определены и могут принимать любое значение. Это делает все состояния проекта легко доступными для инструмента.
  • Если необходимо, добавьте ограничение, чтобы мог произойти только один импульс сброса, в противном случае он может попробовать 1 сброс, 2 сброса, 3 сброса ...
  • Возможно, вам придется ограничить другие входы бездействием, чтобы он не пытался использовать их для исследования состояний таким образом, но это может быть ненужным.

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

person Paul S    schedule 12.01.2016