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の発表は、このRISC-Vの仕様をHaskellとして表現する、ということ。

riscv-semantic (https://github.com/samuelgruetter/riscv-coq)

ちなみにこれ以外にもFormal表現はたくさんあるらしい (RISC-V Organizationは統一する気は無いのか...)

RISC-V Formal Verification Framework (https://github.com/cliffordwolf/riscv-formal)
RISCV ISA Formal Spec in BSV (https://github.com/rsnikhil/RISCV_ISA_Formal_Spec_in_BSV)
RISCV-ISA-Spec (https://github.com/rsnikhil/RISCV-ISA-Spec)
L3 Specification of the RISC-V ISA (https://github.com/SRI-CSL/l3riscv)

このriscv-semanticでいうと、さらに、CLASHというコンパイラを使うと、Haskellのコードを回路に変換することができる、らしい。

試しにソースコードを見てみる。確かに、すべての命令がHaskellで記述されている。

src/ExecuteM.hs

execute (Mulh rd rs1 rs2) = do
  x <- getRegister rs1
  y <- getRegister rs2
  setRegister rd (highBits ((regToZ_signed x) * (regToZ_signed y)) :: t)

MMUの部分とかは結構分かりやすいのではないだろうか？

src/VirtualMemory.hs

calculateAddress :: (RiscvProgram p t) => AccessType -> MachineInt -> p MachineInt
calculateAddress accessType va = do
  mode <- fmap getMode (getCSRField Field.MODE)
  privMode <- getPrivMode
  mprv <- getCSRField Field.MPRV
  mpp <- getCSRField Field.MPP
  let effectPriv = if mprv == 1 then decodePrivMode mpp else privMode
  if mode == None || (privMode == Machine && accessType == Instruction) || (effectPriv == Machine)
    then return va
    else -- First the translation may be in a cache, possibly stalled, cacheAccess use the typeclass defined "TLB"
      cacheAccess va $
       do
    ppn <- getCSRField Field.PPN
    maybePTE <- findLeafEntry (mode, accessType, va, (shift ppn 12)) (pageTableLevels mode - 1)
    case maybePTE of
      Nothing -> pageFault accessType va
      Just (level, pte, addr) -> do
        let r = testBit pte 1
        let w = testBit pte 2
        let x = testBit pte 3
        let u = testBit pte 4

RISC-V Formal Semantics を使えるようにする

まずは、Haskellのコンパイラ環境であるStackをインストールする。

curl -sSL https://get.haskellstack.org/ | sh
git clone https://github.com/mit-plv/riscv-semantics.git
cd riscv-semantics
./install.sh  # これで何かしら大量にインストールされる

で、make を実行してみるのだが、なんか失敗するじゃないか。

$ make
riscv-none-embed-gcc -march=rv32im -mabi=ilp32 -static -nostdlib -nostartfiles -mcmodel=medany -c init.S -o init32.o
make[1]: riscv-none-embed-gcc: コマンドが見つかりませんでした
Makefile:25: ターゲット 'init32.o' のレシピで失敗しました

そもそも riscv-none-embed-gcc が必要とは書いていないのでこれはおかしいのでは？Makefileを書き直してriscv32-unknown-elf-gcc で書き直してみる。

diff --git a/Makefile b/Makefile
index 4878218..689bf7d 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,9 @@ test:
        $(MAKE) -C test

 riscv-tests:
-       RISCV_PREFIX=riscv-none-embed- $(MAKE) -C riscv-tests/isa rv64mi rv64si rv64ui
+       $(MAKE) -C riscv-tests/isa rv64mi rv64si rv64ui
+
+#      RISCV_PREFIX=riscv-none-embed- $(MAKE) -C riscv-tests/isa rv64mi rv64si rv64ui

 clean:
        rm -rf .stack-work/
diff --git a/test/Makefile b/test/Makefile
index e325f2f..289857a 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -12,8 +12,8 @@ HEX32=$(addsuffix .hex,$(ELF32))
 HEX64=$(addsuffix .hex,$(ELF64))
 ELF2HEX=../elf2hex

-RISCVCC64=riscv-none-embed-gcc -march=rv64im -mabi=lp64 -static -nostdlib -nostartfiles -mcmodel=medany
-RISCVCC32=riscv-none-embed-gcc -march=rv32im -mabi=ilp32 -static -nostdlib -nostartfiles -mcmodel=medany
+RISCVCC64=riscv32-unknown-elf-gcc -march=rv64im -mabi=lp64 -static -nostdlib -nostartfiles -mcmodel=medany
+RISCVCC32=riscv32-unknown-elf-gcc -march=rv32im -mabi=ilp32 -static -nostdlib -nostartfiles -mcmodel=medany

 all: $(HEX32) $(HEX64)

これで通るようになった。makeを実行するとテストパタンセットがすべてコンパイルされた？

ただし、ここから先のHaskellの実行がうまく行かない。Haskellについてはあまりに無知なのだが、何か間違っているのだろうか？

stack exec riscv-semantics test/build/thuemorse32.hex
Executable named riscv-semantics not found on path: ["/home/msyksphinz/work/formal/riscv-semantics/.stack-work/install/x86_64-linux/nightly-2017-10-26/8.2.1/bin","/home/msyksphinz/.stack/snapshots/x86_64-linux/nightly-2017-10-26/8.2.1/bin","/home/msyksphinz/.stack/compiler-tools/x86_64-linux/ghc-8.2.1/bin","/home/msyksphinz/.stack/programs/x86_64-linux/ghc-8.2.1/bin"...