Continuing Towards a Trustworthy Stack : Formal Verification of Correctness for Data Forwarding in an In-Order Pipelined Processor Circuit for a RISC ISA

Sammanfattning

To increase the performance, modern processor pipelines heavily rely on data forwarding, a technique to avoid pipeline stalls by adding additional data paths that route computed values to future instructions elsewhere in the pipeline before the instruction that produced that value has been fully processed. However, this adds complexity, making it harder to trust the correctness of such pipelined circuits. This thesis presents an approach to improve the performance of an in-order pipelined RISC processor architecture using data forwarding with guaranteed functional correctness down to its circuit-level implementation. We show that the processor executes program instructions correctly according to their specification, by proving a refinement relation between the execution traces of the processor circuit and the abstract behaviour of the instruction set architecture. The proof is mechanised using the HOL4 interactive theorem prover. The formally verified circuit has been successfully synthesised as a small computer system, integrating other unverified components like a cache and interrupt handler, for the PYNQ-Z1 FPGA board. The benchmarks indicate that the presented processor circuit outperforms the original processor. To the best of our knowledge, this thesis presents the fastest open-source processor with guaranteed functional correctness down to the circuit level.