Формальная модель представляет из себя набор
формальных правил работы проекта. Наиболее
известной реализацией формальной модели являются
конструкции SystemVerilog Assertions.
Например, следующая конструкция: A |-> ## [0:10] (B || C) ;
означает, что если сигнал A равен True, то или сигнал B, или сигнал C должен быть хотябы один раз равен True в течение 10 тактов с момента установки A в True.
Особенностью данной конструкции является то,
что если сигнал B всегда равен True, то сигнал C никогда не тестируется. Поэтому ещё потребуются
конструкции covergroup и coverpoint, которые будут отслеживать, чтобы в процессе моделирования
сигнал B переключался во все возможные состояния
заданное количество раз и с заданными интервалами.
Автоматизация моделирования с применением формальной модели является одним из отличий "Верификации" от простого "Моделирования".
