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, functional-verification, formal logical and comparative-analytical methods, which made it possible to distinguish between scenario-based 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'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