PAFSV: A process algebraic framework for systemVerilog

K. L. Man

doi:10.1109/IMCSIT.2008.4747295

PAFSV: A process algebraic framework for systemVerilog

K. L. Man

University College Cork

Research output: Chapter in Book or Report/Conference proceeding › Conference Proceeding › peer-review

3 Citations (Scopus)

Abstract

We develop a process algebraic framework, called process algebraic framework for IEEE 1800™ SystemVerilog (PAFSV), for 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 some examples: A MUX, a synchronous reset D flip-flop and an arbiter.

Original language	English
Title of host publication	Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008
Pages	535-542
Number of pages	8
DOIs	https://doi.org/10.1109/IMCSIT.2008.4747295
Publication status	Published - 2008
Externally published	Yes
Event	International Multiconference on Computer Science and Information Technology, IMCSIT 2008 - Wisla, Poland Duration: 20 Oct 2008 → 22 Oct 2008

Publication series

Name	Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008
Volume	3

Conference

Conference	International Multiconference on Computer Science and Information Technology, IMCSIT 2008
Country/Territory	Poland
City	Wisla
Period	20/10/08 → 22/10/08

Access to Document

10.1109/IMCSIT.2008.4747295

Cite this

Man, K. L. (2008). PAFSV: A process algebraic framework for systemVerilog. In Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008 (pp. 535-542). Article 4747295 (Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008; Vol. 3). https://doi.org/10.1109/IMCSIT.2008.4747295

@inproceedings{b40d009044f64365b3b81d32a5b67952,

title = "PAFSV: A process algebraic framework for systemVerilog",

abstract = "We develop a process algebraic framework, called process algebraic framework for IEEE 1800{\texttrademark} SystemVerilog (PAFSV), for 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 some examples: A MUX, a synchronous reset D flip-flop and an arbiter.",

author = "Man, {K. L.}",

year = "2008",

doi = "10.1109/IMCSIT.2008.4747295",

language = "English",

isbn = "9788360810149",

series = "Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008",

pages = "535--542",

booktitle = "Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008",

note = "International Multiconference on Computer Science and Information Technology, IMCSIT 2008 ; Conference date: 20-10-2008 Through 22-10-2008",

}

Man, KL 2008, PAFSV: A process algebraic framework for systemVerilog. in Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008., 4747295, Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008, vol. 3, pp. 535-542, International Multiconference on Computer Science and Information Technology, IMCSIT 2008, Wisla, Poland, 20/10/08. https://doi.org/10.1109/IMCSIT.2008.4747295

PAFSV: A process algebraic framework for systemVerilog. / Man, K. L.
Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008. 2008. p. 535-542 4747295 (Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008; Vol. 3).

Research output: Chapter in Book or Report/Conference proceeding › Conference Proceeding › peer-review

TY - GEN

T1 - PAFSV

T2 - International Multiconference on Computer Science and Information Technology, IMCSIT 2008

AU - Man, K. L.

PY - 2008

Y1 - 2008

N2 - We develop a process algebraic framework, called process algebraic framework for IEEE 1800™ SystemVerilog (PAFSV), for 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 some examples: A MUX, a synchronous reset D flip-flop and an arbiter.

AB - We develop a process algebraic framework, called process algebraic framework for IEEE 1800™ SystemVerilog (PAFSV), for 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 some examples: A MUX, a synchronous reset D flip-flop and an arbiter.

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

U2 - 10.1109/IMCSIT.2008.4747295

DO - 10.1109/IMCSIT.2008.4747295

M3 - Conference Proceeding

AN - SCOPUS:70349320618

SN - 9788360810149

T3 - Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008

SP - 535

EP - 542

BT - Proceedings of the International Multiconference on Computer Science and Information Technology, IMCSIT 2008

Y2 - 20 October 2008 through 22 October 2008

ER -

PAFSV: A process algebraic framework for systemVerilog

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this