В диссертационном исследовании разработаны модели и методы функциональной верификации цифровых систем на кристаллах на основе использования темпоральных ассерций для тестового диагностирования ошибок в процессе программно-аппаратного моделирования, обеспечивающего существенное повышение качества цифрового изделия, а также уменьшение временных и материальных затрат проектирования. Разработана аналитическая модель верификации цифровых систем на основе использования динамических регистровых очередей для анализа ассерций линейной темпоральной логики. Усовершенствована модель взаимодействия данных регистрового уровня, а также модель процесса верификации и диагностирования путем аппаратной поддержки моделирования и введения в программный код ассерционной избыточности.