Specification and analysis of Null Convention Logic (NCL) circuits using PAFSV

Ka Lok Man; Nan Zhang; Chi Un Lei; Eng Gee Lim; T. O. Ting; Kaiyu Wan; Jieming Ma; Tomas Krilavičius; Dawei Liu; Yu Guo

Specification and analysis of Null Convention Logic (NCL) circuits using PAFSV

Ka Lok Man
, Nan Zhang
, Chi Un Lei
, Eng Gee Lim
, T. O. Ting
, Kaiyu Wan
, Jieming Ma
, Tomas Krilavičius
, Dawei Liu
, Yu Guo

The University of Hong Kong
Baltic Institute of Advanced Technology
University of Science and Technology of China

Research output: Contribution to journal › Conference article › peer-review

Abstract

In this work, a process algebraic framework known as PAFSV is applied to the formal specication and analysis of IEEE 1800TM SystemVerilog design. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. In addition, a set of properties of PAFSV is defined for a notion of bisimilarity; and PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. The main aim of this paper is to demonstrate that PAFSV is effective and useful for the formal specification and analysis of IEEE 1800TM SystemVerilog design. To achieve the aim of this approach, we apply PAFSV to model and analyse classical circuits such as the Null Convention Logic (NCL) circuit.

Original language	English
Journal	Lecture Notes in Engineering and Computer Science
Volume	2210
Issue number	January
Publication status	Published - 2014
Event	International MultiConference of Engineers and Computer Scientists, IMECS 2014 - Kowloon, Hong Kong Duration: 12 Mar 2014 → 14 Mar 2014

Keywords

Formal language
Formal semantics
Null Convention Logic (NCL)
Systemverilog

Cite this

@article{b01765c2b0aa466aabf960beda21cbb6,

title = "Specification and analysis of Null Convention Logic (NCL) circuits using PAFSV",

abstract = "In this work, a process algebraic framework known as PAFSV is applied to the formal specication and analysis of IEEE 1800TM SystemVerilog design. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. In addition, a set of properties of PAFSV is defined for a notion of bisimilarity; and PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. The main aim of this paper is to demonstrate that PAFSV is effective and useful for the formal specification and analysis of IEEE 1800TM SystemVerilog design. To achieve the aim of this approach, we apply PAFSV to model and analyse classical circuits such as the Null Convention Logic (NCL) circuit.",

keywords = "Formal language, Formal semantics, Null Convention Logic (NCL), Systemverilog",

author = "Man, \{Ka Lok\} and Nan Zhang and Lei, \{Chi Un\} and Lim, \{Eng Gee\} and Ting, \{T. O.\} and Kaiyu Wan and Jieming Ma and Tomas Krilavi{\v c}ius and Dawei Liu and Yu Guo",

year = "2014",

language = "English",

volume = "2210",

journal = "Lecture Notes in Engineering and Computer Science",

issn = "2078-0958",

number = "January",

note = "International MultiConference of Engineers and Computer Scientists, IMECS 2014 ; Conference date: 12-03-2014 Through 14-03-2014",

}

TY - JOUR

T1 - Specification and analysis of Null Convention Logic (NCL) circuits using PAFSV

AU - Man, Ka Lok

AU - Zhang, Nan

AU - Lei, Chi Un

AU - Lim, Eng Gee

AU - Ting, T. O.

AU - Wan, Kaiyu

AU - Ma, Jieming

AU - Krilavičius, Tomas

AU - Liu, Dawei

AU - Guo, Yu

PY - 2014

Y1 - 2014

N2 - In this work, a process algebraic framework known as PAFSV is applied to the formal specication and analysis of IEEE 1800TM SystemVerilog design. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. In addition, a set of properties of PAFSV is defined for a notion of bisimilarity; and PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. The main aim of this paper is to demonstrate that PAFSV is effective and useful for the formal specification and analysis of IEEE 1800TM SystemVerilog design. To achieve the aim of this approach, we apply PAFSV to model and analyse classical circuits such as the Null Convention Logic (NCL) circuit.

AB - In this work, a process algebraic framework known as PAFSV is applied to the formal specication and analysis of IEEE 1800TM SystemVerilog design. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. In addition, a set of properties of PAFSV is defined for a notion of bisimilarity; and PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. The main aim of this paper is to demonstrate that PAFSV is effective and useful for the formal specification and analysis of IEEE 1800TM SystemVerilog design. To achieve the aim of this approach, we apply PAFSV to model and analyse classical circuits such as the Null Convention Logic (NCL) circuit.

KW - Formal language

KW - Formal semantics

KW - Null Convention Logic (NCL)

KW - Systemverilog

UR - https://www.scopus.com/pages/publications/84938311488

M3 - Conference article

AN - SCOPUS:84938311488

SN - 2078-0958

VL - 2210

JO - Lecture Notes in Engineering and Computer Science

JF - Lecture Notes in Engineering and Computer Science

IS - January

T2 - International MultiConference of Engineers and Computer Scientists, IMECS 2014

Y2 - 12 March 2014 through 14 March 2014

ER -

Specification and analysis of Null Convention Logic (NCL) circuits using PAFSV

Abstract

Keywords

Other files and links

Fingerprint

Cite this