PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog

Authors

  • Ka Lok Man Department of Computer Science and Software Engineering, Xi'an Jiaotong-Liverpool University, Suzhou
  • Chi-Un Lei The University of Hong Kong
  • Hemangee K. Kapoor Indian Institute of Technology Guwahati
  • Tomas Krilavicius Vytautas Magnus University, Lithuania & Baltic Institute of Advanced Technology
  • Jieming Ma Suzhou University of Science and Technology
  • Nan Zhang Department of Computer Science and Software Engineering, Xi'an Jiaotong-Liverpool University, China & CITIC Securities

Keywords:

SystemVerilog, process algebras, formal semantics, PAFSV, formal specification and analysis, circuit verification

Abstract

We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800TM SystemVerilog designs. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. A set of properties of PAFSV is presented for a notion of bisimilarity. PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800TM SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.

Downloads

Download data is not yet available.

Downloads

Published

2016-05-31

How to Cite

Man, K. L., Lei, C.-U., Kapoor, H. K., Krilavicius, T., Ma, J., & Zhang, N. (2016). PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog. Computing and Informatics, 35(1), 143–176. Retrieved from http://147.213.75.17/ojs/index.php/cai/article/view/1371

Issue

Vol. 35 No. 1 (2016): Computing and Informatics

Section

Articles