Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL

Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational semantics for MDESL. This article investigates the soundness and completeness of the operational semantics for MDESL based on the denotational semantics. We introduce the concepts of transitional condition and phase semantics for each transition to show the relationship between a transition and variables in the denotational model. Then, we give the definition for the soundness and completeness of the operational semantics for MDESL. Based on our definition of the operational semantics of MDESL, we investigate the detailed theoretical proof for the soundness and completeness. Finally, a practical approach complements the theoretical one. We apply the proof assistant Coq to verify the soundness and completeness of the operational semantics for MDESL. Our research demonstrates the consistency between operational and denotational semantics for MDESL through theoretical and practical approaches.