PAFSV: A formal framework for specification and analysis of SystemVerilog

Ka Lok Man; Chi Un Lei; Hemangee K. Kapoor; Tomas Krilavičius; Jieming Ma; Nan Zhang

PAFSV: A formal framework for specification and analysis of SystemVerilog

Ka Lok Man, Chi Un Lei, Hemangee K. Kapoor, Tomas Krilavičius, Jieming Ma, Nan Zhang

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800^™ 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 1800^™ SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800^™ SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.

Original language	English
Pages (from-to)	143-176
Number of pages	34
Journal	Computing and Informatics
Volume	35
Issue number	1
Publication status	Published - 2016

Keywords

Circuit verification
Formal semantics
Formal specification and analysis
PAFSV
Process algebras
SystemVerilog

Cite this

@article{86545e8f184e4141997a5c129b10f152,

title = "PAFSV: A formal framework for specification and analysis of SystemVerilog",

abstract = "We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800{\texttrademark} 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 1800{\texttrademark} SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800{\texttrademark} SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.",

keywords = "Circuit verification, Formal semantics, Formal specification and analysis, PAFSV, Process algebras, SystemVerilog",

author = "Man, {Ka Lok} and Lei, {Chi Un} and Kapoor, {Hemangee K.} and Tomas Krilavi{\v c}ius and Jieming Ma and Nan Zhang",

year = "2016",

language = "English",

volume = "35",

pages = "143--176",

journal = "Computing and Informatics",

issn = "1335-9150",

number = "1",

}

TY - JOUR

T1 - PAFSV

T2 - A formal framework for specification and analysis of SystemVerilog

AU - Man, Ka Lok

AU - Lei, Chi Un

AU - Kapoor, Hemangee K.

AU - Krilavičius, Tomas

AU - Ma, Jieming

AU - Zhang, Nan

PY - 2016

Y1 - 2016

N2 - We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800™ 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 1800™ SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800™ SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.

AB - We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800™ 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 1800™ SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800™ SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.

KW - Circuit verification

KW - Formal semantics

KW - Formal specification and analysis

KW - PAFSV

KW - Process algebras

KW - SystemVerilog

UR - http://www.scopus.com/inward/record.url?scp=84974808858&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:84974808858

SN - 1335-9150

VL - 35

SP - 143

EP - 176

JO - Computing and Informatics

JF - Computing and Informatics

IS - 1

ER -

PAFSV: A formal framework for specification and analysis of SystemVerilog

Abstract

Keywords

Other files and links

Cite this