Hardware composition with hardware flowcharts and process algebras
Juin-Yeu Lu, Jang Dae Kim, Shiu‐Kai Chin · 2002
Algorithmic state machine (ASM) descriptions or hardware flowcharts have been used successfully to describe and verify large systems like the IBM 3081. Hardware flowcharts are intuitively appealing in their specification of control flow and data path operations. Nevertheless, previous mechanizations of hardware flowcharts lacked a formal semantics which prevented a rigorous analysis of implementations refined from ASM descriptions, and the ability to equate composed ASM descriptions to purely behavioral descriptions. To address these concerns, we describe an algorithmic register transfer language which has a formal semantics along with an algebra which is used to reason about composed ASM descriptions.