FPGA開発日記

カテゴリ別記事インデックス https://msyksphinz.github.io/github_pages , English Version https://fpgadevdiary.hatenadiary.com/

RISC-Vのフォーマル検証環境riscv-formalを試す

RISC-V
https://content.riscv.org/wp-content/uploads/2018/06/Symbiotic-EDA-300x66.png

RISC-V Summitで発表があったRISC-VのFormalツールに、riscv-formalというものがある。

内容はまだ未確認だが、どうやらRISC-Vのプロセッサに対してFormal検証をかけることができるツールらしい。

github.com

もともとこのツールはVerilogなど通常のデザインに対して有効である。

例えば、以下のような検証ができる。

  • demo.sv
module demo (
  input clk,
  output [5:0] counter
);
  reg [5:0] counter = 0;

  always @(posedge clk) begin
    if (counter == 15)
      counter <= 0;
    else
      counter <= counter + 1;
  end

`ifdef FORMAL
  always @(posedge clk) begin
    assert (counter < 32);
  end
`endif
endmodule

FORMALで記述されているassert文が検証対象となる。

  • demo.sby
[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -formal demo.sv
prep -top demo

[files]
demo.sv

同じように、32-bit RISC-Vプロセッサについてフォーマル検証が可能だ。

まずは、riscv-formalを使うための環境をビルドする。基本的には、以下のサイトを参照に構築すればよい。

Getting Started — SymbiYosys 0.1 documentation

ただし、一つだけabcのビルドには、リポジトリのアップデートが必要だった。extavyのサブモジュールであるabcを最新のリビジョン(c935e76 : 2018/12/07時点) にアップデートする。

次に、picorv32をダウンロードして、Formal検証ツールを流してみよう。

  git clone https://github.com/SymbioticEDA/riscv-formal.git
  cd riscv-formal/cores/picorv32/
  wget -O picorv32.v https://raw.githubusercontent.com/cliffordwolf/picorv32/master/picorv32.v
  python3 ../../checks/genchecks.py
  make -C checks -j$(nproc)

これで60本程度のテストパタンが流れ始める。エラー無く終了すればOK。

SBY  0:24:03 [insn_xori_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:35 (95)
SBY  0:24:03 [insn_xori_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:33 (93)
SBY  0:24:03 [insn_xori_ch0] summary: engine_0 (smtbmc boolector) returned PASS
SBY  0:24:03 [insn_xori_ch0] DONE (PASS, rc=0)
SBY  0:25:04 [insn_sw_ch0] engine_0: ##   0:03:21  Status: PASSED
SBY  0:25:04 [insn_sw_ch0] engine_0: finished (returncode=0)
SBY  0:25:04 [insn_sw_ch0] engine_0: Status returned by engine: PASS
SBY  0:25:04 [insn_sw_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:03:27 (207)
SBY  0:25:04 [insn_sw_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:03:20 (200)
SBY  0:25:04 [insn_sw_ch0] summary: engine_0 (smtbmc boolector) returned PASS
SBY  0:25:04 [insn_sw_ch0] DONE (PASS, rc=0)
make: Leaving directory '/home/msyksphinz/work/riscv/riscv-formal/cores/picorv32/checks'
$

picorv32.vを見てみると、FORMAL用の外部に出力する信号が定義してあった。

module picorv32 #(
        parameter [ 0:0] ENABLE_COUNTERS = 1,
...
        // IRQ Interface
        input      [31:0] irq,
        output reg [31:0] eoi,

`ifdef RISCV_FORMAL
        output reg        rvfi_valid,
        output reg [63:0] rvfi_order,
        output reg [31:0] rvfi_insn,
        output reg        rvfi_trap,
        output reg        rvfi_halt,
        output reg        rvfi_intr,
        output reg [ 1:0] rvfi_mode,
        output reg [ 4:0] rvfi_rs1_addr,
        output reg [ 4:0] rvfi_rs2_addr,
        output reg [31:0] rvfi_rs1_rdata,
        output reg [31:0] rvfi_rs2_rdata,
        output reg [ 4:0] rvfi_rd_addr,
        output reg [31:0] rvfi_rd_wdata,
        output reg [31:0] rvfi_pc_rdata,
        output reg [31:0] rvfi_pc_wdata,
        output reg [31:0] rvfi_mem_addr,
        output reg [ 3:0] rvfi_mem_rmask,
        output reg [ 3:0] rvfi_mem_wmask,
        output reg [31:0] rvfi_mem_rdata,
        output reg [31:0] rvfi_mem_wdata,
`endif

        // Trace Interface

例えばADD命令を検証するためのsbyは以下のようになっている。

  • checks/insn_add_ch0.sby
[options]
mode bmc
append 0
tbtop wrapper.uut
depth 21
skip 20

[engines]
smtbmc boolector

[script]
read_verilog -sv insn_add_ch0.sv
read_verilog -sv /home/msyksphinz/work/riscv/riscv-formal/cores/picorv32/../../cores/picorv32/wrapper.sv
read_verilog /home/msyksphinz/work/riscv/riscv-formal/cores/picorv32/../../cores/picorv32/picorv32.v
prep -flatten -nordff -top rvfi_testbench
...
[file insn_add_ch0.sv]
`include "defines.sv"
`include "rvfi_channel.sv"
`include "rvfi_testbench.sv"
`include "rvfi_insn_check.sv"
`include "insn_add.v"
  • checks/insn_add_ch0/src/insn_add.v
module rvfi_insn_add (
  input                                 rvfi_valid,
  input  [`RISCV_FORMAL_ILEN   - 1 : 0] rvfi_insn,
  input  [`RISCV_FORMAL_XLEN   - 1 : 0] rvfi_pc_rdata,
  input  [`RISCV_FORMAL_XLEN   - 1 : 0] rvfi_rs1_rdata,
  input  [`RISCV_FORMAL_XLEN   - 1 : 0] rvfi_rs2_rdata,
  input  [`RISCV_FORMAL_XLEN   - 1 : 0] rvfi_mem_rdata,
`ifdef RISCV_FORMAL_CSR_MISA
  input  [`RISCV_FORMAL_XLEN   - 1 : 0] rvfi_csr_misa_rdata,
  output [`RISCV_FORMAL_XLEN   - 1 : 0] spec_csr_misa_rmask,
`endif

  output                                spec_valid,
  output                                spec_trap,
  output [                       4 : 0] spec_rs1_addr,
  output [                       4 : 0] spec_rs2_addr,
  output [                       4 : 0] spec_rd_addr,
  output [`RISCV_FORMAL_XLEN   - 1 : 0] spec_rd_wdata,
  output [`RISCV_FORMAL_XLEN   - 1 : 0] spec_pc_wdata,
  output [`RISCV_FORMAL_XLEN   - 1 : 0] spec_mem_addr,
  output [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_mem_rmask,
  output [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_mem_wmask,
  output [`RISCV_FORMAL_XLEN   - 1 : 0] spec_mem_wdata
);
...
  // ADD instruction
  wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs1_rdata + rvfi_rs2_rdata;
  assign spec_valid = rvfi_valid && !insn_padding && insn_funct7 == 7'b 0000000 && insn_funct3 == 3'b 000 && insn_opcode == 7'b 0110011;
  assign spec_rs1_addr = insn_rs1;
  assign spec_rs2_addr = insn_rs2;
  assign spec_rd_addr = insn_rd;
  assign spec_rd_wdata = spec_rd_addr ? result : 0;
  assign spec_pc_wdata = rvfi_pc_rdata + 4;

ここには、ADD命令のパタンが書き込まれている。これに基づいて検証が行われているわけか。