[libre-riscv-dev] [Bug 340] New: formal proof of POWER9 SHIFTROT pipeline needed