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

Hongyan Zhao, Huibiao Zhu, Feng Sheng, Jifeng He, Jonathan Bowen

Research output: Contribution to journalArticlepeer-review

Abstract

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 paper 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.
Original languageEnglish
Number of pages53
JournalFormal Aspects of Computing
Early online date25 Sept 2024
DOIs
Publication statusPublished - 25 Sept 2024
Externally publishedYes

Cite this