The Verification of MDG Algorithms in the HOL Theorem Prover

Formal verification of digital systems is
achieved, today, using one of two main approaches: states
exploration (mainly model checking (MC)) or deductive
reasoning (theorem proving). The combination of the two
approaches promises to overcome the limitation and to
enhance the capabilities of each. Our research is motivated
by this goal. In this book, we provide the necessary
infrastructure (data structure + algorithms) to define high
level states exploration in the HOL theorem prover named as
MDG-HOL platform. We have based our approach on Multiway
Decision Graphs (MDGs). We formalize the basic MDG
operations within HOL following a deep embedding approach.
Then, we derive the correctness proof for each MDG basic
operator. Based on this platform, the MDG reachability
analysis is defined in HOL as a conversion that uses the MDG
theory within HOL. Finally, we propose a reduction
technique to improve MDGs MC based on MDG-HOL platform. The
idea is to prune the transition relation of the circuits
using pre-proved theorems from the specification given at
system level. We use the consistency of the specifications
to verify if the reduced model is faithful to the original
one.