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.
Publié le : 2016-05-31
Classification:
Theoretical Foundations,
SystemVerilog, process algebras, formal semantics, PAFSV, formal specification and analysis, circuit verification,
68Q45
@article{cai1371,
author = {Ka Lok Man; Department of Computer Science and Software Engineering, Xi'an Jiaotong-Liverpool University, Suzhou and Chi-Un Lei; The University of Hong Kong and Hemangee K. Kapoor; Indian Institute of Technology Guwahati and Tomas Krilavicius; Vytautas Magnus University, Lithuania \& Baltic Institute of Advanced Technology and Jieming Ma; Suzhou University of Science and Technology and Nan Zhang; Department of Computer Science and Software Engineering, Xi'an Jiaotong-Liverpool University, China \& CITIC Securities},
title = {PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog},
journal = {Computing and Informatics},
volume = {34},
number = {4},
year = {2016},
language = {en},
url = {http://dml.mathdoc.fr/item/cai1371}
}
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. PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog. Computing and Informatics, Tome 34 (2016) no. 4, . http://gdmltest.u-ga.fr/item/cai1371/