DocumentCode
3076751
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
fYear
2011
fDate
27-29 June 2011
Firstpage
1
Lastpage
2
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/SSIRI-C.2011.10
Filename
6004491
Link To Document