Метою дослідження було теоретичне обґрунтування сутності функціональної та формальної верифікації цифрових систем, порівняння їхніх методів і визначення можливостей узгодженого застосування до цифрових модулів різної структурної складності. Установлено, що функціональна верифікація забезпечувала перевірку поведінкової відповідності цифрового модуля специфікації через тестові впливи, очікувані вихідні реакції, тестбенчі, симуляцію та аналіз покриття функціональних режимів. Формальна верифікація формувала інший тип перевірочного висновку, оскільки була спрямована на підтвердження або спростування властивостей коректності, інваріантів, логічних і часових умов, допустимих переходів та недосяжності помилкових станів. Експериментально-демонстраційна перевірка на мультиплексорі, скінченному автоматі та спрощеному інтерфейсному контролері показала, що зі зростанням складності цифрового модуля збільшувалася кількість функціональних сценаріїв, ускладнювалося покриття режимів і зростав ризик невиявлення прихованих станів, блокувань або рідкісних комбінацій сигналів. Обґрунтовано доцільність комбінованої стратегії, у якій функціональні сценарії, аналіз покриття, формальні властивості та інтерпретація можливих контрприкладів взаємно доповнюють один одного.