PipelineGen: Towards Automated Generation of Pipeline from ISA Formal Semantic Specification

Currently, there are numerous manual factors in microprocessor pipeline design, which may cause problems such as ambiguity in design understanding, low development efficiency, and proneness to errors. In this paper, we propose a method for automatically generating an in-order and single-issue pipeline from formal semantic descriptions of instruction set architecture of a given microprocessor. Based on a divide-and-conquer strategy, an individual datapath for each instruction is synthesized first, and then the datapaths of all instructions are composed into a single datapath using signals-reuse and various proposed techniques, to generate the final pipeline.We implement the proposed method as an open source tool - PipelineGen, which realizes a complete tool-chain from instruction set formal specification to RTL code, and enriches the ecosystem of the Sail language. We evaluate PipelineGen using three typical microprocessor ISAs. PipelineGen can generate correct pipeline designs in minutes, verifying the core concept of "synthesis is correct". The promising experimental results demonstrate that our method effectively alleviates the problems in manual pipeline design.