Вперше запропоновано аналітичну модель верифікації HDL-коду, яка характеризується використанням динамічних регістрових черг у разі аналізу темпоральних асерцій в процесі моделювання тестів цифрових систем на кристалах, що забезпечує збільшення швидкодії моделювання та глибини діагностування помилок коду. Вперше надано модель інтерпретації лінійної темпоральної логіки з використанням режиму глобального часу, яка характеризується наявністю складних семантичних операторів, що дозволяє розширити функціональні можливості динамічної верифікації до підмножини операторів рівня формальних методів. Встановлено методи аналізу механізму асерцій з використанням предикторних зв'язків і зворотного повідомлення, направлені на зменшення кількості транспортовуваних подій, які характеризуються додатковими структурними зв'язками та лініями спостереження, що дозволяє підвищити швидкодію моделювання та зменшити час верифікації проекту. Вдосконалено модель взаємодії даних регістрового рівня та побудовані на ній процес-моделі обробки послідовностей подій та функцій-черг, які відрізняються константною обчислювальною складністю завдяки непрямій інтерпретації індексів і використанню контейнера подій, що забезпечує зменшення структурної складності програмної реалізації моделі динамічних регістрових черг. Запропоновано модель процесу верифікації та діагностування проектованого виробу, яка відрізняється введенням в код програмної надлишковості у вигляді асерцій й апаратною підтримкою моделювання, що дозволяє можливість істотно зменшити загальний час проектування цифрових систем на кристалах.

  Скачати повний текст