Отечественные БМК, технологии проектирования Опции

[Stas]

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