RISC-V Formal Verification Framework (riscv-formal) についてまとめる (13. VexRiscvにCLZ命令を実装する)

前回の記事では、riscv-formalフレームワークを使用してVexRiscvの動作確認を行った。今回は、RISC-V Zbb拡張のCLZ（Count Leading Zeros）命令をVexRiscvに実装し、riscv-formalで検証する。

CLZ命令は、RISC-V Zbb拡張（Bit Manipulation Extension）に含まれる命令で、32ビット値の先頭ゼロビット数をカウントする。

VexRiscvへの実装

1. 命令定義の追加

まず、Riscv.scalaにCLZ命令の定義を追加した：

// Bit manipulation instructions (Zbb extension)
def CLZ = M"0110000----------001-----0010011"

2. IntAluPluginの拡張

IntAluPlugin.scalaを修正してCLZ命令を処理できるようにした：

object AluBitwiseCtrlEnum extends SpinalEnum(binarySequential){
  val XOR, OR, AND, CLZ = newElement()
}

3. デコード処理の追加

CLZ命令のデコード処理を追加：

CLZ -> (immediateActions ++ List(ALU_CTRL -> AluCtrlEnum.BITWISE, ALU_BITWISE_CTRL -> AluBitwiseCtrlEnum.CLZ))

4. 実行処理の実装

先頭ゼロビットカウントの実装：

def countLeadingZeros(value: Bits): UInt = {
  val leadingZeros = UInt(32 bits)

  // Simple implementation using when-elsewhen chain
  when(value(31)) {
    leadingZeros := 0
  } elsewhen (value(30)) {
    leadingZeros := 1
  } elsewhen (value(29)) {
    leadingZeros := 2
  }
  // ... (各ビット位置に対応)
  } elsewhen (value(0)) {
    leadingZeros := 31
  } otherwise {
    leadingZeros := 32
  }

  leadingZeros
}

ビルドとテスト

実装後、VexRiscvをビルドして動作確認を行った：

cd VexRiscv
sbt "runMain vexriscv.demo.FormalSimple"

ビルドは成功した。