TY - GEN
T1 - An instruction set process calculus
AU - Chin, Shiu Kai
AU - Kim, Jang Dae
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1998.
PY - 1998
Y1 - 1998
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84949009274&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84949009274&partnerID=8YFLogxK
U2 - 10.1007/3-540-49519-3_29
DO - 10.1007/3-540-49519-3_29
M3 - Conference contribution
AN - SCOPUS:84949009274
SN - 3540651918
SN - 9783540651918
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 451
EP - 468
BT - Formal Methods in Computer-Aided Design - 2nd International Conference, FMCAD 1998, Proceedings
A2 - Gopalakrishnan, Ganesh
A2 - Windley, Phillip
PB - Springer Verlag
T2 - 2nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 1998
Y2 - 4 November 1998 through 6 November 1998
ER -