Формальная модель

Формальная модель представляет из себя набор формальных правил работы проекта. Наиболее известной реализацией формальной модели являются конструкции SystemVerilog Assertions.

Например, следующая конструкция:
A |-> ## [0:10] (B || C) ;
означает, что если сигнал A равен True, то или сигнал B, или сигнал C должен быть хотябы один раз равен True в течение 10 тактов с момента установки A в True.

Особенностью данной конструкции является то, что если сигнал B всегда равен True, то сигнал C никогда не тестируется. Поэтому ещё потребуются конструкции covergroup и coverpoint, которые будут отслеживать, чтобы в процессе моделирования сигнал B переключался во все возможные состояния заданное количество раз и с заданными интервалами.

Автоматизация моделирования с применением формальной модели является одним из отличий "Верификации" от простого "Моделирования".

Подробнее о Верификации >>