Methods of functional and formal verification of digital systems: Theoretical analysis and experimental application to modules of varying complexity

Abstract

The study aimed to provide a theoretical justification of the nature of functional and formal verification of digital systems, to compare their methods, and to determine the possibilities for their coordinated application to digital modules of varying structural complexity. Methodology was based on normative-terminological, structural-analytical, functionalverification, formal logical and comparative-analytical methods, which made it possible to distinguish between scenariobased and property-based approaches to verifying hardware logic and to conduct an experimental and demonstrative verification of three test digital modules. The study established that functional verification ensured the verification of a digital module&039;s behavioural compliance with the specification through test inputs, expected output responses, test benches, simulation and analysis of functional mode coverage. Formal verification yielded a different type of verification conclusion, as it was aimed at confirming or refuting correctness properties, invariants, logical and temporal conditions, valid transitions and the unreachability of erroneous states. Experimental and demonstrative verification on a multiplexer, a finite-state machine and a simplified interface controller showed that, as the complexity of the digital module increased, the number of functional scenarios grew, mode coverage became more challenging, and the risk of failing to detect hidden states, deadlocks or rare signal combinations increased. For the multiplexer, both approaches yielded consistent results; for the finite-state machine, the verification of resets, states and transitions was enhanced; for the interface controller, formal verification improved the assessment of deadlocks, signal conflicts and erroneous modes. The feasibility of a combined strategy, in which functional scenarios, coverage analysis, formal properties and the interpretation of possible counterexamples complement one another, has been demonstrated. The practical significance of the results is determined by their application in digital design, hardware verification and educational and research environments for planning the verification of digital modules, refining specifications, conducting coverage analysis, interpreting counterexamples and making decisions regarding the correctness of hardware logic.

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