Verilog程序的命题投影时序逻辑符号模型检测  

Symbolic model checking of Verilog programs with the propositional projection temporal logic

作　　者：逄涛 段振华[1,2] 刘晓芳[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071 [2]西安电子科技大学综合业务网理论及关键技术国家重点实验室,陕西西安710071

出　　处：《西安电子科技大学学报》2014年第2期79-84,共6页Journal of Xidian University

基　　金：国家重点基础研究发展计划(973)资助项目(2010CB328102);国家自然科学基金资助项目(61133001)

摘　　要：为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法.依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程序进行验证,从而证明片上系统满足设计规范.以Verilog程序描述的四位同步二进制计数系统的验证实例表明,Verilog程序的命题投影时序逻辑符号模型检测方法是可行的.To insure the correctness of the system on chip （SoC） designed in the Verilog hardware description language, a symbolic model checking methodology for Verilog programs is proposed. With this methodology, the Verilog program to be verified is modeled as a finite-state machine with respect to its formal operational semantics, while the design specifications are expressed in propositional projection temporal logic（PPTL） formulas. Whether the SoC satisfies its specifications or not can be determined with the symbolic model checker proposed in our previous work. A case of a 4-bit synchronous binary counting system described in Verilog programs is studied to illustrate the feasibility of this methodology.

关 键 词：时序逻辑 符号模型检测 硬件描述语言 片上系统验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]