Formal Specification of RTL-Level Digital System Using Projection Temporal Logic

Peng Fei Zhang

doi:10.4028/www.scientific.net/AMM.719-720.949

Paper Titles

Research on the Parallel Frequent Data Mining Strategy under the Cloud Computing Environment
p.924

Application and Discussion of Cloud Computing in Academic Libraries
p.929

A Research of the Essence of SQL Injection Attacks Vulnerability
p.935

Tensors Method Based Method of RF Fingerprints Identification
p.941

Formal Specification of RTL-Level Digital System Using Projection Temporal Logic
p.949

The Image Processing Algorithm of Surface Topography Based on Laser Interference Measurement
p.959

An Image Segmentation Calculation Based on Differential Box-Counting of Fractal Geometry
p.964

The Comparison and Analysis of SEMG in Upper Limb Movement between Hemiplegic Patients and Healthy People
p.969

The Design of Traffic Statistics System Based on Video
p.973

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 719-720Formal Specification of RTL-Level Digital System...

Formal Specification of RTL-Level Digital System Using Projection Temporal Logic

Abstract:

An approach to specify a RTL-level system using Projection Temporal Logic (PTL) is proposed in this paper. With this approach, a digital system described with Register Transfer Language can be translated into PTL formulae, and properties of the system can be specified by PTL either. Then MSVL(Modeling, Simulation and Verification Language) can be used for detecting the error of the design formally.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 719-720)

Pages:

949-955

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.719-720.949

Citation:

Cite this paper

Online since:

January 2015

Authors:

Peng Fei Zhang

Keywords:

Formal Specification, Formal Verification, Projection Temporal Logic, Register Transfer Language

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] John D. Carpinelli, Computer Systems Organization and Architecture, 1st edition, Addison-Wesley Longman Publishing Co., (2000).

Google Scholar

[2] Jurgen Ruf, Roland J. Weiss, Thomas Kropf, and Wolfgang Rosenstiel, Modeling and Formal Verification of Production Automation Systems, INT2004, LNCS3174, springer verlag, 2004, pp.541-566.

Google Scholar

[3] X. Liu, H. Yang, H. Zedan, Formal methods for the re-engineering of computing systems: a comparison, " Computer Software and Applications Conference, 1997. COMPSAC , 97. Proceedings, The Twenty-First Annual International, Aug, 1997, pp: 409-414.

DOI: 10.1109/cmpsac.1997.625024

Google Scholar

[4] Z. Duan, Temporal Logic and Temporal Logic Programming, Science Press, Beijing, ISBN: 7-03-016651-5/TP. 3158, (2006).

Google Scholar

[5] B. Moszkowski, Executing Temporal Logic Programs, Cambridge University Press, (1986).

Google Scholar

[6] Zhenhua Duan, Cong Tian, A Unified Model Checking Approach with Projection Temporal Logic, ICFEM2008, LNCS5256, Springer-verlag, Oct, 2008, pp.167-186.

Google Scholar

[7] SHU Xin-Feng, DUAN Zhen-Hua, Complete Axiomatization for Projection Temporal Logic with Finite Time, Journal of Software, 2011, 22(3): 366-380.

DOI: 10.3724/sp.j.1001.2011.03918

Google Scholar

[8] YANG Xiao-xiao, DUAN Zhen-hua, Verification of programs based on an axiom for the MSVL language, Journal of Xidian University, vol. 37, No. 1, Feb. 2010, pp: 96-101.

Google Scholar

[9] Duan ZH, Tian C. A unified model checking approach with projection temporal logic, " In: Proc. of the 10th Int, l Conf. on Formal Engineering Methods (ICFEM 2008). LNCS 5256, Berlin: Springer-Verlag, 2008. 167−186. [doi: 10. 1007/978-3-540-88194-0_12].

DOI: 10.1007/978-3-540-88194-0_12

Google Scholar

[10] WANG Xiao bing, DUAN Zhenhua, Projection Temporal Logic Oriented Model Checking for Web Services, " Jounal of Xi, an Jiaotong University, vol. 43, No. 4, Apr. 2009, pp: 39-43.

Google Scholar