Title :
Towards Denotational Semantics for Verilog in PVS
Author :
Zhu, Han ; Zhu, Huibiao ; Liu, Si ; Guo, Jian
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Abstract :
Verilog is a hardware description language that has been widely used in industry. We have explored its denotational semantics, operational semantics and algebraic semantics. In order to support the mechanical proof for the properties of Verilog programs, this paper studies the mechanical approach to the denotational semantics. We apply PVS in this exploration. Based on this achievement, algebraic laws for Verilog programs can be verified in the PVS framework.
Keywords :
hardware description languages; programming language semantics; PVS framework; Verilog; algebraic semantics; denotational semantics; hardware description language; operational semantics; Concurrent computing; Continuous time systems; Hardware; Hardware design languages; Joining processes; Medical services; Semantics; Denotational Semantics; PVS; Verilog;
Conference_Titel :
Secure Software Integration & Reliability Improvement Companion (SSIRI-C), 2011 5th International Conference on
Conference_Location :
Jeju Island
Print_ISBN :
978-1-4577-0781-0
Electronic_ISBN :
978-0-7695-4454-0
DOI :
10.1109/SSIRI-C.2011.10
