Generating designs using an algorithmic register transfer language with formal semantics

Juin Yeu Lu; Shiu Kai Chin

doi:10.1007/3-540-58450-1_51

Generating designs using an algorithmic register transfer language with formal semantics

Juin Yeu Lu, Shiu Kai Chin

Department of Electrical Engineering & Computer Science

Research output: Chapter in Book/Entry/Poem › Conference contribution

Abstract

ARTL (Algorithmic Register Transfer Language) is a language used to describe and specify synchronous hardware at the algorithmic and register-transfer levels. Its syntax and natural semantics are formalized in higher-order logic using HOL. An ARTL simulation engine (abstract machine) and compiler are described and verified within HOL. The machine and compiler for ARTL is fully implemented. Also, we present the principles of ARTL synthesis using to standard cells and field programmable gate arrays (FPGAs).

Original language	English (US)
Title of host publication	Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings
Editors	Thomas F. Melham, Juanito Camilleri
Publisher	Springer Verlag
Pages	316-331
Number of pages	16
ISBN (Print)	9783540584506
DOIs	https://doi.org/10.1007/3-540-58450-1_51
State	Published - 1994
Event	7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994 - Valletta, Malta Duration: Sep 19 1994 → Sep 22 1994

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	859 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994
Country/Territory	Malta
City	Valletta
Period	9/19/94 → 9/22/94

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-58450-1_51

Cite this

Lu, J. Y., & Chin, S. K. (1994). Generating designs using an algorithmic register transfer language with formal semantics. In T. F. Melham, & J. Camilleri (Eds.), Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings (pp. 316-331). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 859 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-58450-1_51

Generating designs using an algorithmic register transfer language with formal semantics. / Lu, Juin Yeu; Chin, Shiu Kai.
Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings. ed. / Thomas F. Melham; Juanito Camilleri. Springer Verlag, 1994. p. 316-331 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 859 LNCS).

Research output: Chapter in Book/Entry/Poem › Conference contribution

Lu, JY & Chin, SK 1994, Generating designs using an algorithmic register transfer language with formal semantics. in TF Melham & J Camilleri (eds), Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 859 LNCS, Springer Verlag, pp. 316-331, 7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994, Valletta, Malta, 9/19/94. https://doi.org/10.1007/3-540-58450-1_51

Lu JY, Chin SK. Generating designs using an algorithmic register transfer language with formal semantics. In Melham TF, Camilleri J, editors, Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings. Springer Verlag. 1994. p. 316-331. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-58450-1_51

Lu, Juin Yeu ; Chin, Shiu Kai. / Generating designs using an algorithmic register transfer language with formal semantics. Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings. editor / Thomas F. Melham ; Juanito Camilleri. Springer Verlag, 1994. pp. 316-331 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1f9b75ff00334c85ac7b01c987ce47d4,

title = "Generating designs using an algorithmic register transfer language with formal semantics",

abstract = "ARTL (Algorithmic Register Transfer Language) is a language used to describe and specify synchronous hardware at the algorithmic and register-transfer levels. Its syntax and natural semantics are formalized in higher-order logic using HOL. An ARTL simulation engine (abstract machine) and compiler are described and verified within HOL. The machine and compiler for ARTL is fully implemented. Also, we present the principles of ARTL synthesis using to standard cells and field programmable gate arrays (FPGAs).",

author = "Lu, {Juin Yeu} and Chin, {Shiu Kai}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994 ; Conference date: 19-09-1994 Through 22-09-1994",

year = "1994",

doi = "10.1007/3-540-58450-1_51",

language = "English (US)",

isbn = "9783540584506",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "316--331",

editor = "Melham, {Thomas F.} and Juanito Camilleri",

booktitle = "Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings",

}

TY - GEN

T1 - Generating designs using an algorithmic register transfer language with formal semantics

AU - Lu, Juin Yeu

AU - Chin, Shiu Kai

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - ARTL (Algorithmic Register Transfer Language) is a language used to describe and specify synchronous hardware at the algorithmic and register-transfer levels. Its syntax and natural semantics are formalized in higher-order logic using HOL. An ARTL simulation engine (abstract machine) and compiler are described and verified within HOL. The machine and compiler for ARTL is fully implemented. Also, we present the principles of ARTL synthesis using to standard cells and field programmable gate arrays (FPGAs).

AB - ARTL (Algorithmic Register Transfer Language) is a language used to describe and specify synchronous hardware at the algorithmic and register-transfer levels. Its syntax and natural semantics are formalized in higher-order logic using HOL. An ARTL simulation engine (abstract machine) and compiler are described and verified within HOL. The machine and compiler for ARTL is fully implemented. Also, we present the principles of ARTL synthesis using to standard cells and field programmable gate arrays (FPGAs).

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

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

U2 - 10.1007/3-540-58450-1_51

DO - 10.1007/3-540-58450-1_51

M3 - Conference contribution

AN - SCOPUS:85027398361

SN - 9783540584506

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 316

EP - 331

BT - Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings

A2 - Melham, Thomas F.

A2 - Camilleri, Juanito

PB - Springer Verlag

T2 - 7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994

Y2 - 19 September 1994 through 22 September 1994

ER -

Generating designs using an algorithmic register transfer language with formal semantics

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this