Modeling and verification of NCL circuits using PAT

Jieming Ma; Ka Lok Man; Eng Gee Lim; Nan Zhang; Chi Un Lei; Sheng Uei Guan; Taikyeong Ted Jeong; Jong Kug Seon

doi:10.1016/j.proeng.2011.08.639

Modeling and verification of NCL circuits using PAT

Jieming Ma^*
, Ka Lok Man
, Eng Gee Lim
, Nan Zhang
, Chi Un Lei
, Sheng Uei Guan
, Taikyeong Ted Jeong
, Jong Kug Seon

^*Corresponding author for this work

The University of Hong Kong
Myongji University
LG Corporation

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

Abstract

NULL Conventional Logic (NCL) is a Delay-Insensitive (DI) clockless paradigm and is suitable for implementing asynchronous circuits. Efficient methods of analysis are required to specify and verify such DI systems. Based on Delay Insensitive sequential Process (DISP) specification, this paper demonstrates the application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify the behavior of NCL circuits. A few useful constructs are successfully modeled and verified by using PAT. The flexibility and simplicity of the coding, simulation and verification shows that PAT is effective and applicable for NCL circuit design and verification.

Original language	English
Pages (from-to)	3411-3415
Number of pages	5
Journal	Procedia Engineering
Volume	15
DOIs	https://doi.org/10.1016/j.proeng.2011.08.639
Publication status	Published - 2011
Event	2011 International Conference on Advanced in Control Engineering and Information Science, CEIS 2011 - Dali, Yunnam, China Duration: 18 Aug 2011 → 19 Aug 2011

Keywords

CSP#
NCL circuits
Specification
Verfication

Access to Document

10.1016/j.proeng.2011.08.639

Cite this

@article{637b000db75d44e39fb57df4302e54ec,

title = "Modeling and verification of NCL circuits using PAT",

abstract = "NULL Conventional Logic (NCL) is a Delay-Insensitive (DI) clockless paradigm and is suitable for implementing asynchronous circuits. Efficient methods of analysis are required to specify and verify such DI systems. Based on Delay Insensitive sequential Process (DISP) specification, this paper demonstrates the application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify the behavior of NCL circuits. A few useful constructs are successfully modeled and verified by using PAT. The flexibility and simplicity of the coding, simulation and verification shows that PAT is effective and applicable for NCL circuit design and verification.",

keywords = "CSP\#, NCL circuits, Specification, Verfication",

author = "Jieming Ma and Man, \{Ka Lok\} and Lim, \{Eng Gee\} and Nan Zhang and Lei, \{Chi Un\} and Guan, \{Sheng Uei\} and Jeong, \{Taikyeong Ted\} and Seon, \{Jong Kug\}",

year = "2011",

doi = "10.1016/j.proeng.2011.08.639",

language = "English",

volume = "15",

pages = "3411--3415",

journal = "Procedia Engineering",

note = "2011 International Conference on Advanced in Control Engineering and Information Science, CEIS 2011 ; Conference date: 18-08-2011 Through 19-08-2011",

}

TY - JOUR

T1 - Modeling and verification of NCL circuits using PAT

AU - Ma, Jieming

AU - Man, Ka Lok

AU - Lim, Eng Gee

AU - Zhang, Nan

AU - Lei, Chi Un

AU - Guan, Sheng Uei

AU - Jeong, Taikyeong Ted

AU - Seon, Jong Kug

PY - 2011

Y1 - 2011

N2 - NULL Conventional Logic (NCL) is a Delay-Insensitive (DI) clockless paradigm and is suitable for implementing asynchronous circuits. Efficient methods of analysis are required to specify and verify such DI systems. Based on Delay Insensitive sequential Process (DISP) specification, this paper demonstrates the application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify the behavior of NCL circuits. A few useful constructs are successfully modeled and verified by using PAT. The flexibility and simplicity of the coding, simulation and verification shows that PAT is effective and applicable for NCL circuit design and verification.

AB - NULL Conventional Logic (NCL) is a Delay-Insensitive (DI) clockless paradigm and is suitable for implementing asynchronous circuits. Efficient methods of analysis are required to specify and verify such DI systems. Based on Delay Insensitive sequential Process (DISP) specification, this paper demonstrates the application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify the behavior of NCL circuits. A few useful constructs are successfully modeled and verified by using PAT. The flexibility and simplicity of the coding, simulation and verification shows that PAT is effective and applicable for NCL circuit design and verification.

KW - CSP#

KW - NCL circuits

KW - Specification

KW - Verfication

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

U2 - 10.1016/j.proeng.2011.08.639

DO - 10.1016/j.proeng.2011.08.639

M3 - Conference article

AN - SCOPUS:84055200461

VL - 15

SP - 3411

EP - 3415

JO - Procedia Engineering

JF - Procedia Engineering

T2 - 2011 International Conference on Advanced in Control Engineering and Information Science, CEIS 2011

Y2 - 18 August 2011 through 19 August 2011

ER -

Modeling and verification of NCL circuits using PAT

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this