An instruction set process calculus

Shiu Kai Chin, Jang Dae Kim

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We have created a calculus for reasoning about hardware and firmware at the algorithmic state machine (ASM) and instruction-set processor (ISP) levels of description. The calculus is a value-passing process algebra that extends the Mealy machine model to include paral-lel composition. It supports reasoning about the composed behavior of synchronous ASM and ISP components and microcode. We present an overview of the calculus and its application including an example show-ing the equivalence of a microcoded machine to its target instruction set specified by both ASM and ISP descriptions. The calculus, its properties, and the examples have been deeply embedded, proved, and verified as conservative extensions to the logic of the Higher Order Logic (HOL90) theorem prover.

Original languageEnglish (US)
Title of host publicationFormal Methods in Computer-Aided Design - 2nd International Conference, FMCAD 1998, Proceedings
EditorsGanesh Gopalakrishnan, Phillip Windley
PublisherSpringer Verlag
Pages451-468
Number of pages18
ISBN (Print)3540651918, 9783540651918
DOIs
StatePublished - 1998
Event2nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 1998 - Palo Alto, United States
Duration: Nov 4 1998Nov 6 1998

Publication series

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

Other

Other2nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 1998
CountryUnited States
CityPalo Alto
Period11/4/9811/6/98

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'An instruction set process calculus'. Together they form a unique fingerprint.

Cite this