Formal specification of an asynchronous processor via action refinement
Xiuli Sun, Xiaoyu Song, Jinzhao Wu, Mila Majster-Cederbaum · 2006
With the purpose of providing a formal specification of pipelines, a central problem in asynchronous hardware design, we show how action refinement can be used to develop asynchronous pipelined microprocessors, where each functional unit of the processor is stepwise obtained, leading to a structured and modular design. Furthermore, the handling of hazard situations is realized during the refinement procedures.