RISC-V Formal Verification Framework (riscv-formal) についてまとめる (5. VexRiscvのFormalの解析)
VexRiscv におけるriscv-formal の実行方法を調査している。 前回の続き：msyksphinz.hatenablog.com 例えば、 rvfi_insn_addi は以下のようにインスタンス化されている。それぞれのフォーマルの項目に対してインスタンスが作られているようだ。 insns/isa_rv64imc.v wire spec_insn_addi_valid; wire spec_insn_addi_trap…
