TY - GEN
T1 - Towards denotational semantics for verilog in PVS
AU - Zhu, Han
AU - Zhu, Huibiao
AU - Liu, Si
AU - Guo, Jian
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/80053006355
U2 - 10.1109/SSIRI-C.2011.10
DO - 10.1109/SSIRI-C.2011.10
M3 - 会议稿件
AN - SCOPUS:80053006355
SN - 9780769544540
T3 - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011
SP - 1
EP - 2
BT - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011
T2 - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011
Y2 - 27 June 2011 through 29 June 2011
ER -