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

doi:10.3969/j.issn.1001-2400.2014.02.013

J4 ›› 2014, Vol. 41 ›› Issue (2): 79-84.doi: 10.3969/j.issn.1001-2400.2014.02.013

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

逄涛^1,2;段振华^1,2;刘晓芳^1,2

(1. 西安电子科技大学计算理论与技术研究所，陕西西安 710071;
2. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安 710071)

收稿日期:2013-06-07 出版日期:2014-04-20 发布日期:2014-05-30
通讯作者: 逄涛
作者简介:逄涛(1984-)，男，西安电子科技大学博士研究生，E-mail：t_pang@126.com．
基金资助:
国家重点基础研究发展计划(973)资助项目(2010CB328102)；国家自然科学基金资助项目(61133001)

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

PANG Tao^1,2;DUAN Zhenhua^1,2;LIU Xiaofang^1,2

(1. Research Inst. of Computing Theory & Technology, Xidian Univ., Xi'an 710071， China;
2. State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China)

Received:2013-06-07 Online:2014-04-20 Published:2014-05-30
Contact: PANG Tao

摘要/Abstract

摘要：

为了保证以Verilog硬件描述语言设计的片上系统的正确性，提出了Verilog程序的符号模型检测方法．依据形式化操作语义将Verilog程序建模为有限状态机，将设计规范用命题投影时序逻辑公式描述，并采用命题投影时序逻辑符号模型检测工具对程序进行验证，从而证明片上系统满足设计规范．以Verilog程序描述的四位同步二进制计数系统的验证实例表明，Verilog程序的命题投影时序逻辑符号模型检测方法是可行的．

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

Abstract:

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.

Key words: temporal logic, symbolic model checking, hardware description language, system on chip verification

中图分类号:

TP301

逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.

PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic[J]. J4, 2014, 41(2): 79-84.

参考文献

［1］ Badawy W, Jullien G. System on Chip for Real Time Applications ［M］. Norwell: Kluwer Academic Publishers,2003.
［2］ IEEE Standard 1364. IEEE Standard Verilog Hardware Description Language ［S］. USA: IEEE Computer Society Press, 2001.
［3］ Brown S, Rose J. Architecture of FPGAs and CPLDs: a Tutorial ［J］. IEEE Design and Test of Computers, 1996, 13(2): 42-57.
［4］舒新峰, 段振华. 投影时序逻辑的公理系统与形式验证［J］. 西安电子科技大学学报, 2009, 36(4): 680-685.
Shu Xinfeng, Duan Zhenhua. Axiomatization for the First-order Projection Temporal Logic and Formal Verifications ［J］. Journal of Xidian University, 2009, 36(4): 680-685.
［5］范全润, 段振华, 徐国培. 用AIG推理检验组合电路的等价性［J］. 西安电子科技大学学报, 2009, 36(5): 877-884.
Fan Quanrun, Duan Zhenhua, Xu Guopei. Combinational Equivalence Checking Based on AIG Reasoning ［J］. Journal of Xidian University, 2009, 36(5): 877-884.
［6］ Clarke E, Grumberg O, Peled D. Model Checking ［M］. Cambridge: MIT Press, 1999: 27-49.
［7］ Duan Z. Temporal Logic and Temporal Logic Programming ［M］. Beijing: Science Press of China, 2006: 9-17.
［8］ Pang T, Duan Z. Symbolic Model Checking for Embedded Systems: a Case Study ［C］//Proceedings of the 2nd International Conference on Computers, Networks, Systems and Industrial Applications. Piscataway: IEEE, 2012: 644-650.
［9］ Pang T, Duan Z, Tian C. Symbolic Model Checking for Propositional Projection Temporal Logic ［C］//Proceedings of Theoretical Aspects of Software Engineering. Washington: IEEE: 2012: 9-16.
［10］ Byrant R. Graph Based Algorithms for Boolean Function Manipulation ［J］. IEEE Transactions on Computers, 1986, 35(8): 677-691.
［11］ Tian C,Duan Z. Expressiveness of Propositional Projection Temporal Logic with Star ［J］. Theoretical Computer Science, 2011, 412(18): 1729-1744.
［12］ Clarke E, Jain H, Kroening D. Predicate Abstraction and Refinement Techniques for Verifying Verilog［R］. Pittsburgh: Carnegie Mellon University, 2004.
［13］ Winskel G. The Formal Semantics of Programming Languages: an Introduction ［M］. Cambridge: MIT Press, 1993.
［14］ McMillan K. Symbolic Model Checking: an Approach to the State Explosion Problem ［D］. Pittsburgh: Carnegie Mellon University,1993.

[1]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[2]	马倩;段振华. MSVL程序的自动定理证明方法[J]. J4, 2016, 43(1): 75-81.
[3]	张南;段振华. 进位保留加法器的命题投影时序逻辑组合验证[J]. J4, 2012, 39(5): 192-196.
[4]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[5]	王小兵;段振华. 框架时序逻辑语言MSVL中面向对象机制的实现[J]. J4, 2010, 37(3): 559-564+575.
[6]	杨潇潇;段振华. MSVL语言的公理系统的程序验证[J]. J4, 2010, 37(1): 96-101.
[7]	舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.
[8]	张海宾;段振华. 区间时序逻辑的模型检查 [J]. J4, 2009, 36(2): 338-342.
[9]	王小兵;段振华. 框架投影时序逻辑程序设计语言中的指针 [J]. J4, 2008, 35(6): 1069-1074.
[10]	张海宾;段振华. 多速率混合系统的模型检查 [J]. J4, 2008, 35(1): 60-648.
[11]	雷丽晖;段振华. 使用扩展区间时序逻辑为并发工作流建模 [J]. J4, 2007, 34(4): 673-680.
[12]	张海宾;段振华. 稠密时间区间时序逻辑的可满足性判定 [J]. J4, 2007, 34(3): 463-467.

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

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

PDF (PC)

赞

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 12

Metrics

本文评价

推荐阅读 0