Abstract

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

Keywords

MSC

68Q45

Cite this article

@article{cai-1371,
  author  = {Ka Lok Man and Chi-Un Lei and Hemangee K. Kapoor and Tomas Krilavičius and Jieming Ma and Nan Zhang},
  title   = {PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog},
  journal = {Computing and Informatics},
  volume  = {35},
  number  = {1},
  pages   = {143--176},
  year    = {2016},
  issn    = {1335-9150},
  url     = {https://cai.type.sk/content/2016/1/pafsv-a-formal-framework-for-specification-and-analysis-of-systemverilog/}
}
Download .bib