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

doi:10.3969/j.issn.1001-2400.2014.02.013

Abstract

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

CLC Number:

TP301

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.

References

［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]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[2]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[3]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[4]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[5]	WANG Xiao-bing;DUAN Zhen-hua. Implementation of objected-oriented mechanism in framed temporal logic language MSVL [J]. J4, 2010, 37(3): 559-564+575.
[6]	YANG Xiao-xiao;DUAN Zhen-hua. Verification of programs based on an axiom system for the MSVL language [J]. J4, 2010, 37(1): 96-101.
[7]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.
[8]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[9]	WANG Xiao-bing;DUAN Zhen-hua. Pointers in framing projection temporal logic programming languages [J]. J4, 2008, 35(6): 1069-1074.
[10]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[11]	LEI Li-hui;DUAN Zhen-hua. Modelling concurrent workflow with the extended interval temporal logic [J]. J4, 2007, 34(4): 673-680.
[12]	ZHANG Hai-bin;DUAN Zhen-hua. Decidability of the dense timed interval temporal logic [J]. J4, 2007, 34(3): 463-467.

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

PDF (PC)

Like

Knowledge

Cited

Abstract

Cite this article

share this article

References

Related Articles 12

Metrics

Comments

Recommended 0