8th RISC-V Workshop in Barcelona で非常に気になったワーキンググループの一つ、RISC-V Formal Specification について調べた。 Formal Group は、 RISC-Vの仕様を、英語で書かれた仕様書としてだけでなく、マシンでもチェック可能なプログラムのような形で表現すること。 実際、RISC-Vの仕様書はすべての命令が英語の文章として記述されており、正式なDescriptionとして記述されてないので非常に気になっていた。 MITによるFormal Semanticsの発表。発表資料は[リンク先](https://content.riscv.org/wp-content/uploads/2018/05/slidesThomasBourgeat.pdf)を参照。 今回の 8th RISC-V Workshop でのMITの発表は、こ