Пробовали проект под отечественный БМК верифицировать с пакетом "Невод". В итоге поняли, что "Невод' ругается на любую структуру, имеющую обратные связи - типа автомата и др. Видимо это вызвано различием времени Tsetup / Thold в триггерах проекта и разбегом тактового. Как выход предлагается триггера представлять в виде структуры мастер - помощник, те первый работает по нарастающему фронту, второй по спадающему. На сколько это правильно ?
Какие современные пакеты, кроме "Невода" умеют проводить временной анализ по методу Монте - Карло (те случайным образом менять задержку случайной логической цепи и оценивать работоспособность проекта) ?
Речь идет о скомпилированном, но не разведенном на кристалле проекте.

По поводу первой части вопроса - надо смотреть схему (или описание).
Есть какие-то неточности. Автоматы такого типа работали...

Случайным образом задержку никто (я не встречал) не меняет (да и зачем?).
В Невод-е она не совсем случайная (псевдослучайная).

Вообще, лучше моделировать описание в любой современной системе использующей
язык , например, verilog.

Замена свойства псевдослучайности в этом случае - это увеличение в библиотеке времён
в контролях $setup (например в два раза) а $hold - на ненулевой.
Можно добавить другие контроли типа $recovery $width и др.
Иными словами решаем задачу проверки на "вшивость" другим современным способом.

Это всё конечно возможно, если есть verilog-описание БМК-шной библиотеки.