Диссертационная работа посвящена анализу моделей микроархитектуры систем на кристалле на ранних этапах разработки, с целью получения надежных оценок задержки передачи данных. Помимо задачи получения оценок решается задача их формальной верификации за малое время с использованием стандартных средств. Актуальность задачи объясняется потребностью сокращения сроков разработки и снижения стоимости систем на кристалле.