Authors : Hee-Jun Yoo and Jin-Young Choi
Abstract: We describes high-level description of the timing behavior and resource constraints of pipelined out-of-order superscalar processors using formal methods. The parallelism of superscalar processors depends on not only the complexity of hardware functional units but also data dependency between instructions because the processor can do multi- ple instruction issue. So, it`s not easy to analyze and predict the timing properties of these superscalar programs. Here, we present formal meth- ods to illustrate instruction-level modelling of operation of superscalar processors using ACSR which is a process algebra, one of the methodol- ogy in the ?eld of formal methods which can describe and verify system behaviors. ACSR features value passing and built-in concepts of priority, time and resource. With this we can express the superscalar instructions as ACSR processes consuming cpu registers as shared resources and il- lustrate register usage at each cpu execution cycle.
Hee-Jun Yoo and Jin-Young Choi , 2004. Process Algebraic Model of Out-of-Order Superscalar Processor Programs for Instruction Level Timing Analysis . Asian Journal of Information Technology, 3: 1295-1300.