Generating designs using an algorithmic register transfer language with formal semantics

Juin Yeu Lu, Shiu Kai Chin

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings
EditorsThomas F. Melham, Juanito Camilleri
PublisherSpringer Verlag
Pages316-331
Number of pages16
ISBN (Print)9783540584506
DOIs
StatePublished - 1994
Event7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994 - Valletta, Malta
Duration: Sep 19 1994Sep 22 1994

Publication series

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

Other

Other7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994
CountryMalta
CityValletta
Period9/19/949/22/94

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Generating designs using an algorithmic register transfer language with formal semantics'. Together they form a unique fingerprint.

  • 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