From 3e527b37271fae7c3fb03f7a1ba20369d2c71cab Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Thu, 20 Aug 2020 17:28:09 +0800 Subject: [PATCH 1/4] Refactor instructions to use NamedTuple --- rvfi/insns/insn.py | 49 +++++++++++++-------------- rvfi/insns/insn_add.py | 4 +-- rvfi/insns/insn_addi.py | 4 +-- rvfi/insns/insn_and.py | 4 +-- rvfi/insns/insn_andi.py | 4 +-- rvfi/insns/insn_auipc.py | 4 +-- rvfi/insns/insn_beq.py | 6 ++-- rvfi/insns/insn_bge.py | 6 ++-- rvfi/insns/insn_bgeu.py | 6 ++-- rvfi/insns/insn_blt.py | 6 ++-- rvfi/insns/insn_bltu.py | 6 ++-- rvfi/insns/insn_bne.py | 6 ++-- rvfi/insns/insn_jal.py | 9 ++--- rvfi/insns/insn_jalr.py | 9 ++--- rvfi/insns/insn_lb.py | 4 +-- rvfi/insns/insn_lbu.py | 4 +-- rvfi/insns/insn_lh.py | 4 +-- rvfi/insns/insn_lhu.py | 4 +-- rvfi/insns/insn_lui.py | 4 +-- rvfi/insns/insn_lw.py | 4 +-- rvfi/insns/insn_or.py | 4 +-- rvfi/insns/insn_ori.py | 4 +-- rvfi/insns/insn_rv32i_i_type_arith.py | 6 ++-- rvfi/insns/insn_rv32i_i_type_load.py | 13 ++++--- rvfi/insns/insn_rv32i_i_type_shift.py | 8 ++--- rvfi/insns/insn_rv32i_r_type.py | 6 ++-- rvfi/insns/insn_rv32i_s_type.py | 13 ++++--- rvfi/insns/insn_rv32i_sb_type.py | 9 +++-- rvfi/insns/insn_rv32i_u_type.py | 6 ++-- rvfi/insns/insn_sb.py | 4 +-- rvfi/insns/insn_sh.py | 4 +-- rvfi/insns/insn_sll.py | 4 +-- rvfi/insns/insn_slli.py | 4 +-- rvfi/insns/insn_slt.py | 4 +-- rvfi/insns/insn_slti.py | 4 +-- rvfi/insns/insn_sltiu.py | 4 +-- rvfi/insns/insn_sltu.py | 4 +-- rvfi/insns/insn_sra.py | 4 +-- rvfi/insns/insn_srai.py | 4 +-- rvfi/insns/insn_srl.py | 4 +-- rvfi/insns/insn_srli.py | 4 +-- rvfi/insns/insn_sub.py | 4 +-- rvfi/insns/insn_sw.py | 4 +-- rvfi/insns/insn_xor.py | 4 +-- rvfi/insns/insn_xori.py | 4 +-- rvfi/riscv_formal_parameters.py | 4 +++ 46 files changed, 138 insertions(+), 146 deletions(-) create mode 100644 rvfi/riscv_formal_parameters.py diff --git a/rvfi/insns/insn.py b/rvfi/insns/insn.py index b3fbc3e..a47a129 100644 --- a/rvfi/insns/insn.py +++ b/rvfi/insns/insn.py @@ -1,45 +1,42 @@ from nmigen import * """ -Insn.py -Class for generic RISC-V instructions +General RISC-V Instruction """ class Insn(Elaboratable): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - # Core-specific constants - self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN - self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA + def __init__(self, params): + # Core-specific parameters + self.params = params # RVFI input ports self.rvfi_valid = Signal(1) - self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN) - self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN) - if self.RISCV_FORMAL_CSR_MISA: - self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_insn = Signal(self.params.ilen) + self.rvfi_pc_rdata = Signal(self.params.xlen) + self.rvfi_rs1_rdata = Signal(self.params.xlen) + self.rvfi_rs2_rdata = Signal(self.params.xlen) + self.rvfi_mem_rdata = Signal(self.params.xlen) + if self.params.csr_misa: + self.rvfi_csr_misa_rdata = Signal(self.params.xlen) # RVFI output ports - if self.RISCV_FORMAL_CSR_MISA: - self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN) + if self.params.csr_misa: + self.spec_csr_misa_rmask = Signal(self.params.xlen) self.spec_valid = Signal(1) self.spec_trap = Signal(1) self.spec_rs1_addr = Signal(5) self.spec_rs2_addr = Signal(5) self.spec_rd_addr = Signal(5) - self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN) - self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.spec_rd_wdata = Signal(self.params.xlen) + self.spec_pc_wdata = Signal(self.params.xlen) + self.spec_mem_addr = Signal(self.params.xlen) + self.spec_mem_rmask = Signal(int(self.params.xlen // 8)) + self.spec_mem_wmask = Signal(int(self.params.xlen // 8)) + self.spec_mem_wdata = Signal(self.params.xlen) # Additional wires and registers - self.insn_padding = Signal(self.RISCV_FORMAL_ILEN) - self.insn_imm = Signal(self.RISCV_FORMAL_XLEN) + self.insn_padding = Signal(self.params.ilen) + self.insn_imm = Signal(self.params.xlen) self.insn_funct7 = Signal(7) self.insn_funct6 = Signal(6) self.insn_shamt = Signal(6) @@ -59,7 +56,7 @@ class Insn(Elaboratable): self.rvfi_rs2_rdata, self.rvfi_mem_rdata ] - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: input_ports.append(self.rvfi_csr_misa_rdata) output_ports = [ self.spec_valid, @@ -74,7 +71,7 @@ class Insn(Elaboratable): self.spec_mem_wmask, self.spec_mem_wdata ] - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: output_ports.append(self.spec_csr_misa_rmask) return input_ports + output_ports def elaborate(self, platform): diff --git a/rvfi/insns/insn_add.py b/rvfi/insns/insn_add.py index 2cd7f6d..abac425 100644 --- a/rvfi/insns/insn_add.py +++ b/rvfi/insns/insn_add.py @@ -5,8 +5,8 @@ ADD instruction """ class InsnAdd(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b000, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b000, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_addi.py b/rvfi/insns/insn_addi.py index 535990b..b6c3f95 100644 --- a/rvfi/insns/insn_addi.py +++ b/rvfi/insns/insn_addi.py @@ -5,8 +5,8 @@ ADDI instruction """ class InsnAddi(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000) + def __init__(self, params): + super().__init__(params, 0b000) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_and.py b/rvfi/insns/insn_and.py index c82005c..07deb1f 100644 --- a/rvfi/insns/insn_and.py +++ b/rvfi/insns/insn_and.py @@ -5,8 +5,8 @@ AND instruction """ class InsnAnd(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b111, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b111, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_andi.py b/rvfi/insns/insn_andi.py index 17f3660..4e7d1f5 100644 --- a/rvfi/insns/insn_andi.py +++ b/rvfi/insns/insn_andi.py @@ -5,8 +5,8 @@ ANDI instruction """ class InsnAndi(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b111) + def __init__(self, params): + super().__init__(params, 0b111) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_auipc.py b/rvfi/insns/insn_auipc.py index 10c35c4..a5dcd0b 100644 --- a/rvfi/insns/insn_auipc.py +++ b/rvfi/insns/insn_auipc.py @@ -5,8 +5,8 @@ AUIPC instruction """ class InsnAuipc(InsnRV32IUType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0010111) + def __init__(self, params): + super().__init__(params, 0b0010111) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_beq.py b/rvfi/insns/insn_beq.py index a3509ad..5e5944c 100644 --- a/rvfi/insns/insn_beq.py +++ b/rvfi/insns/insn_beq.py @@ -5,12 +5,12 @@ BEQ instruction """ class InsnBeq(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b000) + def __init__(self, params): + super().__init__(params, 0b000) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata == self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_bge.py b/rvfi/insns/insn_bge.py index 94ae31d..8f592df 100644 --- a/rvfi/insns/insn_bge.py +++ b/rvfi/insns/insn_bge.py @@ -5,12 +5,12 @@ BGE instruction """ class InsnBge(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b101) + def __init__(self, params): + super().__init__(params, 0b101) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) >= Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_bgeu.py b/rvfi/insns/insn_bgeu.py index aa91a07..089900e 100644 --- a/rvfi/insns/insn_bgeu.py +++ b/rvfi/insns/insn_bgeu.py @@ -5,12 +5,12 @@ BGEU instruction """ class InsnBgeu(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b111) + def __init__(self, params): + super().__init__(params, 0b111) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata >= self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_blt.py b/rvfi/insns/insn_blt.py index fbb9076..4433e03 100644 --- a/rvfi/insns/insn_blt.py +++ b/rvfi/insns/insn_blt.py @@ -5,12 +5,12 @@ BLT instruction """ class InsnBlt(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b100) + def __init__(self, params): + super().__init__(params, 0b100) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_bltu.py b/rvfi/insns/insn_bltu.py index 9b456a8..0ec2ec4 100644 --- a/rvfi/insns/insn_bltu.py +++ b/rvfi/insns/insn_bltu.py @@ -5,12 +5,12 @@ BLTU instruction """ class InsnBltu(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b110) + def __init__(self, params): + super().__init__(params, 0b110) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_bne.py b/rvfi/insns/insn_bne.py index f28df31..ddfdb59 100644 --- a/rvfi/insns/insn_bne.py +++ b/rvfi/insns/insn_bne.py @@ -5,12 +5,12 @@ BNE instruction """ class InsnBne(InsnRV32ISBType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b001) + def __init__(self, params): + super().__init__(params, 0b001) def elaborate(self, platform): m = super().elaborate(platform) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata != self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok) diff --git a/rvfi/insns/insn_jal.py b/rvfi/insns/insn_jal.py index 0fbfeb5..ac4201d 100644 --- a/rvfi/insns/insn_jal.py +++ b/rvfi/insns/insn_jal.py @@ -5,26 +5,23 @@ JAL instruction """ class InsnJal(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) - self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED def elaborate(self, platform): m = super().elaborate(platform) m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[21:31], self.rvfi_insn[20], self.rvfi_insn[12:20], self.rvfi_insn[31]) << 1)) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) else: m.d.comb += self.misa_ok.eq(1) - if self.RISCV_FORMAL_COMPRESSED: + if self.params.compressed: m.d.comb += self.ialign16.eq(1) else: m.d.comb += self.ialign16.eq(0) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b1101111)) m.d.comb += self.spec_rd_addr.eq(self.insn_rd) diff --git a/rvfi/insns/insn_jalr.py b/rvfi/insns/insn_jalr.py index 0ef1cb5..3966bfc 100644 --- a/rvfi/insns/insn_jalr.py +++ b/rvfi/insns/insn_jalr.py @@ -5,24 +5,21 @@ JALR instruction """ class InsnJalr(InsnRV32IIType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) - self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED def elaborate(self, platform): m = super().elaborate(platform) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) else: m.d.comb += self.misa_ok.eq(1) - if self.RISCV_FORMAL_COMPRESSED: + if self.params.compressed: m.d.comb += self.ialign16.eq(1) else: m.d.comb += self.ialign16.eq(0) - next_pc = Signal(self.RISCV_FORMAL_XLEN) + next_pc = Signal(self.params.xlen) m.d.comb += next_pc.eq((self.rvfi_rs1_rdata + self.insn_imm) & ~1) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b1100111)) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) diff --git a/rvfi/insns/insn_lb.py b/rvfi/insns/insn_lb.py index 6365204..096f47c 100644 --- a/rvfi/insns/insn_lb.py +++ b/rvfi/insns/insn_lb.py @@ -5,5 +5,5 @@ LB instruction """ class InsnLb(InsnRV32IITypeLoad): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1, True) + def __init__(self, params): + super().__init__(params, 0b000, 1, True) diff --git a/rvfi/insns/insn_lbu.py b/rvfi/insns/insn_lbu.py index bf96511..037df22 100644 --- a/rvfi/insns/insn_lbu.py +++ b/rvfi/insns/insn_lbu.py @@ -5,5 +5,5 @@ LBU instruction """ class InsnLbu(InsnRV32IITypeLoad): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b100, 1, False) + def __init__(self, params): + super().__init__(params, 0b100, 1, False) diff --git a/rvfi/insns/insn_lh.py b/rvfi/insns/insn_lh.py index bf09497..9649b30 100644 --- a/rvfi/insns/insn_lh.py +++ b/rvfi/insns/insn_lh.py @@ -5,5 +5,5 @@ LH instruction """ class InsnLh(InsnRV32IITypeLoad): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2, True) + def __init__(self, params): + super().__init__(params, 0b001, 2, True) diff --git a/rvfi/insns/insn_lhu.py b/rvfi/insns/insn_lhu.py index 5e5ca4b..951e501 100644 --- a/rvfi/insns/insn_lhu.py +++ b/rvfi/insns/insn_lhu.py @@ -5,5 +5,5 @@ LHU instruction """ class InsnLhu(InsnRV32IITypeLoad): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b101, 2, False) + def __init__(self, params): + super().__init__(params, 0b101, 2, False) diff --git a/rvfi/insns/insn_lui.py b/rvfi/insns/insn_lui.py index 867f612..93cddd9 100644 --- a/rvfi/insns/insn_lui.py +++ b/rvfi/insns/insn_lui.py @@ -5,8 +5,8 @@ LUI instruction """ class InsnLui(InsnRV32IUType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0110111) + def __init__(self, params): + super().__init__(params, 0b0110111) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_lw.py b/rvfi/insns/insn_lw.py index a9a6117..d6cc21f 100644 --- a/rvfi/insns/insn_lw.py +++ b/rvfi/insns/insn_lw.py @@ -5,5 +5,5 @@ LW instruction """ class InsnLw(InsnRV32IITypeLoad): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4, True) + def __init__(self, params): + super().__init__(params, 0b010, 4, True) diff --git a/rvfi/insns/insn_or.py b/rvfi/insns/insn_or.py index b6d090d..61ececa 100644 --- a/rvfi/insns/insn_or.py +++ b/rvfi/insns/insn_or.py @@ -5,8 +5,8 @@ OR instruction """ class InsnOr(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b110, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b110, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_ori.py b/rvfi/insns/insn_ori.py index 9c8be85..dab6bc4 100644 --- a/rvfi/insns/insn_ori.py +++ b/rvfi/insns/insn_ori.py @@ -5,8 +5,8 @@ ORI instruction """ class InsnOri(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b110) + def __init__(self, params): + super().__init__(params, 0b110) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_i_type_arith.py b/rvfi/insns/insn_rv32i_i_type_arith.py index 4dbc828..65806e5 100644 --- a/rvfi/insns/insn_rv32i_i_type_arith.py +++ b/rvfi/insns/insn_rv32i_i_type_arith.py @@ -5,13 +5,13 @@ RV32I I-Type Instruction (Arithmetic Variation) """ class InsnRV32IITypeArith(InsnRV32IIType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct3): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) + def __init__(self, params, funct3): + super().__init__(params) self.funct3 = funct3 def elaborate(self, platform): m = super().elaborate(platform) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: diff --git a/rvfi/insns/insn_rv32i_i_type_load.py b/rvfi/insns/insn_rv32i_i_type_load.py index 46524da..a1820c5 100644 --- a/rvfi/insns/insn_rv32i_i_type_load.py +++ b/rvfi/insns/insn_rv32i_i_type_load.py @@ -5,30 +5,29 @@ RV32I I-Type Instruction (Load Variation) """ class InsnRV32IITypeLoad(InsnRV32IIType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift, is_signed): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) - self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM + def __init__(self, params, funct3, mask_shift, is_signed): + super().__init__(params) self.funct3 = funct3 self.mask_shift = mask_shift self.is_signed = is_signed - self.addr = Signal(self.RISCV_FORMAL_XLEN) + self.addr = Signal(self.params.xlen) self.result = Signal(8 * self.mask_shift) def elaborate(self, platform): m = super().elaborate(platform) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: m.d.comb += self.misa_ok.eq(1) - if self.RISCV_FORMAL_ALIGNED_MEM: + if self.params.aligned_mem: m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += self.result.eq(self.rvfi_mem_rdata >> (8 * (self.addr - self.spec_mem_addr))) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0000011)) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rd_addr.eq(self.insn_rd) - m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1)) + m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.params.xlen // 8) - 1)) m.d.comb += self.spec_mem_rmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr)) m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.result) if self.is_signed else self.result, 0)) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) diff --git a/rvfi/insns/insn_rv32i_i_type_shift.py b/rvfi/insns/insn_rv32i_i_type_shift.py index ce290b6..37bb303 100644 --- a/rvfi/insns/insn_rv32i_i_type_shift.py +++ b/rvfi/insns/insn_rv32i_i_type_shift.py @@ -5,20 +5,20 @@ RV32I I-Type Instruction (Shift Variation) """ class InsnRV32IITypeShift(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct6, funct3): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) + def __init__(self, params, funct6, funct3): + super().__init__(params) self.funct6 = funct6 self.funct3 = funct3 def elaborate(self, platform): m = super().elaborate(platform) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: m.d.comb += self.misa_ok.eq(1) - m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == self.funct6) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011) & ((~self.insn_shamt[5]) | (self.RISCV_FORMAL_XLEN == 64))) + m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == self.funct6) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011) & ((~self.insn_shamt[5]) | (self.params.xlen == 64))) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rd_addr.eq(self.insn_rd) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) diff --git a/rvfi/insns/insn_rv32i_r_type.py b/rvfi/insns/insn_rv32i_r_type.py index e1964de..c516f82 100644 --- a/rvfi/insns/insn_rv32i_r_type.py +++ b/rvfi/insns/insn_rv32i_r_type.py @@ -5,15 +5,15 @@ RV32I R-Type Instruction """ class InsnRV32IRType(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct7, funct3, opcode): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) + def __init__(self, params, funct7, funct3, opcode): + super().__init__(params) self.funct7 = funct7 self.funct3 = funct3 self.opcode = opcode def elaborate(self, platform): m = super().elaborate(platform) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: diff --git a/rvfi/insns/insn_rv32i_s_type.py b/rvfi/insns/insn_rv32i_s_type.py index 8025ce6..6023237 100644 --- a/rvfi/insns/insn_rv32i_s_type.py +++ b/rvfi/insns/insn_rv32i_s_type.py @@ -5,29 +5,28 @@ RV32I S-Type Instruction """ class InsnRV32ISType(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) - self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM + def __init__(self, params, funct3, mask_shift): + super().__init__(params) self.funct3 = funct3 self.mask_shift = mask_shift - self.addr = Signal(self.RISCV_FORMAL_XLEN) + self.addr = Signal(self.params.xlen) def elaborate(self, platform): m = super().elaborate(platform) m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[7:12], self.rvfi_insn[25:32]))) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: m.d.comb += self.misa_ok.eq(1) - if self.RISCV_FORMAL_ALIGNED_MEM: + if self.params.aligned_mem: m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0100011)) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2) - m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1)) + m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.params.xlen // 8) - 1)) m.d.comb += self.spec_mem_wmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr)) m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata << (8 * (self.addr - self.spec_mem_addr))) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) diff --git a/rvfi/insns/insn_rv32i_sb_type.py b/rvfi/insns/insn_rv32i_sb_type.py index fb11030..c368c15 100644 --- a/rvfi/insns/insn_rv32i_sb_type.py +++ b/rvfi/insns/insn_rv32i_sb_type.py @@ -5,22 +5,21 @@ RV32I SB-Type Instruction """ class InsnRV32ISBType(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, funct3): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) - self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED + def __init__(self, params, funct3): + super().__init__(params) self.funct3 = funct3 def elaborate(self, platform): m = super().elaborate(platform) m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1)) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) else: m.d.comb += self.misa_ok.eq(1) - if self.RISCV_FORMAL_COMPRESSED: + if self.params.compressed: m.d.comb += self.ialign16.eq(1) else: m.d.comb += self.ialign16.eq(0) diff --git a/rvfi/insns/insn_rv32i_u_type.py b/rvfi/insns/insn_rv32i_u_type.py index b755b7c..e76daf5 100644 --- a/rvfi/insns/insn_rv32i_u_type.py +++ b/rvfi/insns/insn_rv32i_u_type.py @@ -5,15 +5,15 @@ RV32I U-Type Instruction """ class InsnRV32IUType(Insn): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, opcode): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA) + def __init__(self, params, opcode): + super().__init__(params) self.opcode = opcode def elaborate(self, platform): m = super().elaborate(platform) m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12)) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.spec_csr_misa_rmask.eq(0) else: diff --git a/rvfi/insns/insn_sb.py b/rvfi/insns/insn_sb.py index 7eb9f4f..c33a1e7 100644 --- a/rvfi/insns/insn_sb.py +++ b/rvfi/insns/insn_sb.py @@ -5,5 +5,5 @@ SB instruction """ class InsnSb(InsnRV32ISType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1) + def __init__(self, params): + super().__init__(params, 0b000, 1) diff --git a/rvfi/insns/insn_sh.py b/rvfi/insns/insn_sh.py index 70cc5b2..dca5cc9 100644 --- a/rvfi/insns/insn_sh.py +++ b/rvfi/insns/insn_sh.py @@ -5,5 +5,5 @@ SH instruction """ class InsnSh(InsnRV32ISType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2) + def __init__(self, params): + super().__init__(params, 0b001, 2) diff --git a/rvfi/insns/insn_sll.py b/rvfi/insns/insn_sll.py index 9832563..c15f502 100644 --- a/rvfi/insns/insn_sll.py +++ b/rvfi/insns/insn_sll.py @@ -5,8 +5,8 @@ SLL instruction """ class InsnSll(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b001, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b001, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slli.py b/rvfi/insns/insn_slli.py index 8d7cf88..36a2712 100644 --- a/rvfi/insns/insn_slli.py +++ b/rvfi/insns/insn_slli.py @@ -5,8 +5,8 @@ SLLI instruction """ class InsnSlli(InsnRV32IITypeShift): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b001) + def __init__(self, params): + super().__init__(params, 0b000000, 0b001) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slt.py b/rvfi/insns/insn_slt.py index 8af854d..588295c 100644 --- a/rvfi/insns/insn_slt.py +++ b/rvfi/insns/insn_slt.py @@ -5,8 +5,8 @@ SLT instruction """ class InsnSlt(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b010, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b010, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slti.py b/rvfi/insns/insn_slti.py index 7a4d364..6377914 100644 --- a/rvfi/insns/insn_slti.py +++ b/rvfi/insns/insn_slti.py @@ -5,8 +5,8 @@ SLTI instruction """ class InsnSlti(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010) + def __init__(self, params): + super().__init__(params, 0b010) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sltiu.py b/rvfi/insns/insn_sltiu.py index 638b6ae..552b552 100644 --- a/rvfi/insns/insn_sltiu.py +++ b/rvfi/insns/insn_sltiu.py @@ -5,8 +5,8 @@ SLTIU instruction """ class InsnSltiu(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b011) + def __init__(self, params): + super().__init__(params, 0b011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sltu.py b/rvfi/insns/insn_sltu.py index 237873c..6e5c477 100644 --- a/rvfi/insns/insn_sltu.py +++ b/rvfi/insns/insn_sltu.py @@ -5,8 +5,8 @@ SLTU instruction """ class InsnSltu(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b011, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b011, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sra.py b/rvfi/insns/insn_sra.py index 56bf8cb..b96bbbb 100644 --- a/rvfi/insns/insn_sra.py +++ b/rvfi/insns/insn_sra.py @@ -5,8 +5,8 @@ SRA instruction """ class InsnSra(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b101, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0100000, 0b101, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srai.py b/rvfi/insns/insn_srai.py index c7b0d27..985f467 100644 --- a/rvfi/insns/insn_srai.py +++ b/rvfi/insns/insn_srai.py @@ -5,8 +5,8 @@ SRAI instruction """ class InsnSrai(InsnRV32IITypeShift): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010000, 0b101) + def __init__(self, params): + super().__init__(params, 0b010000, 0b101) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srl.py b/rvfi/insns/insn_srl.py index 6bc4d1d..6a2cc46 100644 --- a/rvfi/insns/insn_srl.py +++ b/rvfi/insns/insn_srl.py @@ -5,8 +5,8 @@ SRL instruction """ class InsnSrl(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b100, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srli.py b/rvfi/insns/insn_srli.py index 93bb136..e36a907 100644 --- a/rvfi/insns/insn_srli.py +++ b/rvfi/insns/insn_srli.py @@ -5,8 +5,8 @@ SRLI instruction """ class InsnSrli(InsnRV32IITypeShift): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b101) + def __init__(self, params): + super().__init__(params, 0b000000, 0b101) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sub.py b/rvfi/insns/insn_sub.py index 5387b20..a056975 100644 --- a/rvfi/insns/insn_sub.py +++ b/rvfi/insns/insn_sub.py @@ -5,8 +5,8 @@ SUB instruction """ class InsnSub(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b000, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0100000, 0b000, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sw.py b/rvfi/insns/insn_sw.py index 855f3db..120df30 100644 --- a/rvfi/insns/insn_sw.py +++ b/rvfi/insns/insn_sw.py @@ -5,5 +5,5 @@ SW instruction """ class InsnSw(InsnRV32ISType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4) + def __init__(self, params): + super().__init__(params, 0b010, 4) diff --git a/rvfi/insns/insn_xor.py b/rvfi/insns/insn_xor.py index dd5135f..9107836 100644 --- a/rvfi/insns/insn_xor.py +++ b/rvfi/insns/insn_xor.py @@ -5,8 +5,8 @@ XOR instruction """ class InsnXor(InsnRV32IRType): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011) + def __init__(self, params): + super().__init__(params, 0b0000000, 0b100, 0b0110011) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_xori.py b/rvfi/insns/insn_xori.py index 03235c7..d89bceb 100644 --- a/rvfi/insns/insn_xori.py +++ b/rvfi/insns/insn_xori.py @@ -5,8 +5,8 @@ XORI instruction """ class InsnXori(InsnRV32IITypeArith): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA): - super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b100) + def __init__(self, params): + super().__init__(params, 0b100) def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/riscv_formal_parameters.py b/rvfi/riscv_formal_parameters.py new file mode 100644 index 0000000..458469c --- /dev/null +++ b/rvfi/riscv_formal_parameters.py @@ -0,0 +1,4 @@ +from collections import namedtuple + +RISCVFormalParameters = namedtuple('RISCVFormalParameters', + ['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem']) From de3ff25da1b941c7093325b4aaad50dd28982cb1 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Fri, 21 Aug 2020 10:33:02 +0800 Subject: [PATCH 2/4] Refactor insns directory --- rvfi/insns/README.md | 18 ++-- rvfi/insns/insn.py | 2 + rvfi/insns/insn_add.py | 1 + rvfi/insns/insn_addi.py | 1 + rvfi/insns/insn_and.py | 1 + rvfi/insns/insn_andi.py | 1 + rvfi/insns/insn_auipc.py | 1 + rvfi/insns/insn_beq.py | 1 + rvfi/insns/insn_bge.py | 1 + rvfi/insns/insn_bgeu.py | 1 + rvfi/insns/insn_blt.py | 1 + rvfi/insns/insn_bltu.py | 1 + rvfi/insns/insn_bne.py | 1 + rvfi/insns/insn_lui.py | 1 + rvfi/insns/insn_or.py | 1 + rvfi/insns/insn_ori.py | 1 + rvfi/insns/insn_rv32i_i_type_arith.py | 1 + rvfi/insns/insn_rv32i_i_type_load.py | 1 + rvfi/insns/insn_rv32i_i_type_shift.py | 1 + rvfi/insns/insn_rv32i_r_type.py | 1 + rvfi/insns/insn_rv32i_s_type.py | 1 + rvfi/insns/insn_rv32i_sb_type.py | 1 + rvfi/insns/insn_rv32i_u_type.py | 1 + rvfi/insns/insn_sll.py | 1 + rvfi/insns/insn_slli.py | 1 + rvfi/insns/insn_slt.py | 1 + rvfi/insns/insn_slti.py | 1 + rvfi/insns/insn_sltiu.py | 1 + rvfi/insns/insn_sltu.py | 1 + rvfi/insns/insn_sra.py | 1 + rvfi/insns/insn_srai.py | 1 + rvfi/insns/insn_srl.py | 1 + rvfi/insns/insn_srli.py | 1 + rvfi/insns/insn_sub.py | 1 + rvfi/insns/insn_xor.py | 1 + rvfi/insns/insn_xori.py | 1 + rvfi/insns/isa_rv32i.py | 124 +++++++++++++------------- 37 files changed, 106 insertions(+), 72 deletions(-) diff --git a/rvfi/insns/README.md b/rvfi/insns/README.md index 48dd648..00e3768 100644 --- a/rvfi/insns/README.md +++ b/rvfi/insns/README.md @@ -89,14 +89,14 @@ Below is a list of instructions currently supported by this port of the riscv-fo - `IsaRV32I`: RV32I Base ISA -## Core-specific constants +## Core-specific parameters -The following core-specific constants are currently supported: +The following core-specific parameters are currently supported: -| Constant | Description | Valid value(s) | Supported by instruction(s) | Supported by ISA(s) | -| --- | --- | --- | --- | --- | -| `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I | -| `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I | -| `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I | -| `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU | RV32I | -| `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | LB, LH, LW, LBU, LHU, SB, SH, SW | RV32I | +| Constant | Description | Valid value(s) | +| --- | --- | --- | +| `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | +| `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | +| `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | +| `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | +| `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | diff --git a/rvfi/insns/insn.py b/rvfi/insns/insn.py index a47a129..fe7f510 100644 --- a/rvfi/insns/insn.py +++ b/rvfi/insns/insn.py @@ -47,6 +47,7 @@ class Insn(Elaboratable): self.insn_opcode = Signal(7) self.misa_ok = Signal(1) self.ialign16 = Signal(1) + def ports(self): input_ports = [ self.rvfi_valid, @@ -74,6 +75,7 @@ class Insn(Elaboratable): if self.params.csr_misa: output_ports.append(self.spec_csr_misa_rmask) return input_ports + output_ports + def elaborate(self, platform): m = Module() diff --git a/rvfi/insns/insn_add.py b/rvfi/insns/insn_add.py index abac425..54162fc 100644 --- a/rvfi/insns/insn_add.py +++ b/rvfi/insns/insn_add.py @@ -7,6 +7,7 @@ ADD instruction class InsnAdd(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b000, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_addi.py b/rvfi/insns/insn_addi.py index b6c3f95..58aaf52 100644 --- a/rvfi/insns/insn_addi.py +++ b/rvfi/insns/insn_addi.py @@ -7,6 +7,7 @@ ADDI instruction class InsnAddi(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b000) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_and.py b/rvfi/insns/insn_and.py index 07deb1f..e85402e 100644 --- a/rvfi/insns/insn_and.py +++ b/rvfi/insns/insn_and.py @@ -7,6 +7,7 @@ AND instruction class InsnAnd(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b111, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_andi.py b/rvfi/insns/insn_andi.py index 4e7d1f5..cdc7473 100644 --- a/rvfi/insns/insn_andi.py +++ b/rvfi/insns/insn_andi.py @@ -7,6 +7,7 @@ ANDI instruction class InsnAndi(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b111) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_auipc.py b/rvfi/insns/insn_auipc.py index a5dcd0b..bd92a9d 100644 --- a/rvfi/insns/insn_auipc.py +++ b/rvfi/insns/insn_auipc.py @@ -7,6 +7,7 @@ AUIPC instruction class InsnAuipc(InsnRV32IUType): def __init__(self, params): super().__init__(params, 0b0010111) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_beq.py b/rvfi/insns/insn_beq.py index 5e5944c..04e3416 100644 --- a/rvfi/insns/insn_beq.py +++ b/rvfi/insns/insn_beq.py @@ -7,6 +7,7 @@ BEQ instruction class InsnBeq(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b000) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_bge.py b/rvfi/insns/insn_bge.py index 8f592df..a916d42 100644 --- a/rvfi/insns/insn_bge.py +++ b/rvfi/insns/insn_bge.py @@ -7,6 +7,7 @@ BGE instruction class InsnBge(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b101) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_bgeu.py b/rvfi/insns/insn_bgeu.py index 089900e..bfc1798 100644 --- a/rvfi/insns/insn_bgeu.py +++ b/rvfi/insns/insn_bgeu.py @@ -7,6 +7,7 @@ BGEU instruction class InsnBgeu(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b111) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_blt.py b/rvfi/insns/insn_blt.py index 4433e03..0e6c573 100644 --- a/rvfi/insns/insn_blt.py +++ b/rvfi/insns/insn_blt.py @@ -7,6 +7,7 @@ BLT instruction class InsnBlt(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b100) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_bltu.py b/rvfi/insns/insn_bltu.py index 0ec2ec4..bf395d6 100644 --- a/rvfi/insns/insn_bltu.py +++ b/rvfi/insns/insn_bltu.py @@ -7,6 +7,7 @@ BLTU instruction class InsnBltu(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b110) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_bne.py b/rvfi/insns/insn_bne.py index ddfdb59..c4b9964 100644 --- a/rvfi/insns/insn_bne.py +++ b/rvfi/insns/insn_bne.py @@ -7,6 +7,7 @@ BNE instruction class InsnBne(InsnRV32ISBType): def __init__(self, params): super().__init__(params, 0b001) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_lui.py b/rvfi/insns/insn_lui.py index 93cddd9..68689fc 100644 --- a/rvfi/insns/insn_lui.py +++ b/rvfi/insns/insn_lui.py @@ -7,6 +7,7 @@ LUI instruction class InsnLui(InsnRV32IUType): def __init__(self, params): super().__init__(params, 0b0110111) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_or.py b/rvfi/insns/insn_or.py index 61ececa..6f0970f 100644 --- a/rvfi/insns/insn_or.py +++ b/rvfi/insns/insn_or.py @@ -7,6 +7,7 @@ OR instruction class InsnOr(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b110, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_ori.py b/rvfi/insns/insn_ori.py index dab6bc4..a1ba9a6 100644 --- a/rvfi/insns/insn_ori.py +++ b/rvfi/insns/insn_ori.py @@ -7,6 +7,7 @@ ORI instruction class InsnOri(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b110) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_i_type_arith.py b/rvfi/insns/insn_rv32i_i_type_arith.py index 65806e5..c69989c 100644 --- a/rvfi/insns/insn_rv32i_i_type_arith.py +++ b/rvfi/insns/insn_rv32i_i_type_arith.py @@ -8,6 +8,7 @@ class InsnRV32IITypeArith(InsnRV32IIType): def __init__(self, params, funct3): super().__init__(params) self.funct3 = funct3 + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_i_type_load.py b/rvfi/insns/insn_rv32i_i_type_load.py index a1820c5..3ef5e55 100644 --- a/rvfi/insns/insn_rv32i_i_type_load.py +++ b/rvfi/insns/insn_rv32i_i_type_load.py @@ -12,6 +12,7 @@ class InsnRV32IITypeLoad(InsnRV32IIType): self.is_signed = is_signed self.addr = Signal(self.params.xlen) self.result = Signal(8 * self.mask_shift) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_i_type_shift.py b/rvfi/insns/insn_rv32i_i_type_shift.py index 37bb303..d92d2c8 100644 --- a/rvfi/insns/insn_rv32i_i_type_shift.py +++ b/rvfi/insns/insn_rv32i_i_type_shift.py @@ -9,6 +9,7 @@ class InsnRV32IITypeShift(Insn): super().__init__(params) self.funct6 = funct6 self.funct3 = funct3 + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_r_type.py b/rvfi/insns/insn_rv32i_r_type.py index c516f82..a901718 100644 --- a/rvfi/insns/insn_rv32i_r_type.py +++ b/rvfi/insns/insn_rv32i_r_type.py @@ -10,6 +10,7 @@ class InsnRV32IRType(Insn): self.funct7 = funct7 self.funct3 = funct3 self.opcode = opcode + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_s_type.py b/rvfi/insns/insn_rv32i_s_type.py index 6023237..6e4cf9d 100644 --- a/rvfi/insns/insn_rv32i_s_type.py +++ b/rvfi/insns/insn_rv32i_s_type.py @@ -10,6 +10,7 @@ class InsnRV32ISType(Insn): self.funct3 = funct3 self.mask_shift = mask_shift self.addr = Signal(self.params.xlen) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_sb_type.py b/rvfi/insns/insn_rv32i_sb_type.py index c368c15..b68e55e 100644 --- a/rvfi/insns/insn_rv32i_sb_type.py +++ b/rvfi/insns/insn_rv32i_sb_type.py @@ -8,6 +8,7 @@ class InsnRV32ISBType(Insn): def __init__(self, params, funct3): super().__init__(params) self.funct3 = funct3 + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_rv32i_u_type.py b/rvfi/insns/insn_rv32i_u_type.py index e76daf5..4319a09 100644 --- a/rvfi/insns/insn_rv32i_u_type.py +++ b/rvfi/insns/insn_rv32i_u_type.py @@ -8,6 +8,7 @@ class InsnRV32IUType(Insn): def __init__(self, params, opcode): super().__init__(params) self.opcode = opcode + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sll.py b/rvfi/insns/insn_sll.py index c15f502..9263fe5 100644 --- a/rvfi/insns/insn_sll.py +++ b/rvfi/insns/insn_sll.py @@ -7,6 +7,7 @@ SLL instruction class InsnSll(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b001, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slli.py b/rvfi/insns/insn_slli.py index 36a2712..1c8dede 100644 --- a/rvfi/insns/insn_slli.py +++ b/rvfi/insns/insn_slli.py @@ -7,6 +7,7 @@ SLLI instruction class InsnSlli(InsnRV32IITypeShift): def __init__(self, params): super().__init__(params, 0b000000, 0b001) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slt.py b/rvfi/insns/insn_slt.py index 588295c..6504552 100644 --- a/rvfi/insns/insn_slt.py +++ b/rvfi/insns/insn_slt.py @@ -7,6 +7,7 @@ SLT instruction class InsnSlt(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b010, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_slti.py b/rvfi/insns/insn_slti.py index 6377914..a647058 100644 --- a/rvfi/insns/insn_slti.py +++ b/rvfi/insns/insn_slti.py @@ -7,6 +7,7 @@ SLTI instruction class InsnSlti(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b010) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sltiu.py b/rvfi/insns/insn_sltiu.py index 552b552..922bb96 100644 --- a/rvfi/insns/insn_sltiu.py +++ b/rvfi/insns/insn_sltiu.py @@ -7,6 +7,7 @@ SLTIU instruction class InsnSltiu(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sltu.py b/rvfi/insns/insn_sltu.py index 6e5c477..7644099 100644 --- a/rvfi/insns/insn_sltu.py +++ b/rvfi/insns/insn_sltu.py @@ -7,6 +7,7 @@ SLTU instruction class InsnSltu(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b011, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sra.py b/rvfi/insns/insn_sra.py index b96bbbb..6cbc76a 100644 --- a/rvfi/insns/insn_sra.py +++ b/rvfi/insns/insn_sra.py @@ -7,6 +7,7 @@ SRA instruction class InsnSra(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0100000, 0b101, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srai.py b/rvfi/insns/insn_srai.py index 985f467..1e1f6a4 100644 --- a/rvfi/insns/insn_srai.py +++ b/rvfi/insns/insn_srai.py @@ -7,6 +7,7 @@ SRAI instruction class InsnSrai(InsnRV32IITypeShift): def __init__(self, params): super().__init__(params, 0b010000, 0b101) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srl.py b/rvfi/insns/insn_srl.py index 6a2cc46..4f2d2f9 100644 --- a/rvfi/insns/insn_srl.py +++ b/rvfi/insns/insn_srl.py @@ -7,6 +7,7 @@ SRL instruction class InsnSrl(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b100, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_srli.py b/rvfi/insns/insn_srli.py index e36a907..372b05a 100644 --- a/rvfi/insns/insn_srli.py +++ b/rvfi/insns/insn_srli.py @@ -7,6 +7,7 @@ SRLI instruction class InsnSrli(InsnRV32IITypeShift): def __init__(self, params): super().__init__(params, 0b000000, 0b101) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_sub.py b/rvfi/insns/insn_sub.py index a056975..247fed9 100644 --- a/rvfi/insns/insn_sub.py +++ b/rvfi/insns/insn_sub.py @@ -7,6 +7,7 @@ SUB instruction class InsnSub(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0100000, 0b000, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_xor.py b/rvfi/insns/insn_xor.py index 9107836..d5c907d 100644 --- a/rvfi/insns/insn_xor.py +++ b/rvfi/insns/insn_xor.py @@ -7,6 +7,7 @@ XOR instruction class InsnXor(InsnRV32IRType): def __init__(self, params): super().__init__(params, 0b0000000, 0b100, 0b0110011) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/insn_xori.py b/rvfi/insns/insn_xori.py index d89bceb..58d13bd 100644 --- a/rvfi/insns/insn_xori.py +++ b/rvfi/insns/insn_xori.py @@ -7,6 +7,7 @@ XORI instruction class InsnXori(InsnRV32IITypeArith): def __init__(self, params): super().__init__(params, 0b100) + def elaborate(self, platform): m = super().elaborate(platform) diff --git a/rvfi/insns/isa_rv32i.py b/rvfi/insns/isa_rv32i.py index 8b317ea..e98b076 100644 --- a/rvfi/insns/isa_rv32i.py +++ b/rvfi/insns/isa_rv32i.py @@ -41,38 +41,35 @@ RV32I Base ISA """ class IsaRV32I(Elaboratable): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, RISCV_FORMAL_ALIGNED_MEM): - # Core-specific constants - self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN - self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA - self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED - self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM + def __init__(self, params): + # Core-specific parameters + self.params = params # Input ports self.rvfi_valid = Signal(1) - self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN) - self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN) - if self.RISCV_FORMAL_CSR_MISA: - self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_insn = Signal(self.params.ilen) + self.rvfi_pc_rdata = Signal(self.params.xlen) + self.rvfi_rs1_rdata = Signal(self.params.xlen) + self.rvfi_rs2_rdata = Signal(self.params.xlen) + self.rvfi_mem_rdata = Signal(self.params.xlen) + if self.params.csr_misa: + self.rvfi_csr_misa_rdata = Signal(self.params.xlen) # Output ports - if self.RISCV_FORMAL_CSR_MISA: - self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN) + if self.params.csr_misa: + self.spec_csr_misa_rmask = Signal(self.params.xlen) self.spec_valid = Signal(1) self.spec_trap = Signal(1) self.spec_rs1_addr = Signal(5) self.spec_rs2_addr = Signal(5) self.spec_rd_addr = Signal(5) - self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN) - self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.spec_rd_wdata = Signal(self.params.xlen) + self.spec_pc_wdata = Signal(self.params.xlen) + self.spec_mem_addr = Signal(self.params.xlen) + self.spec_mem_rmask = Signal(int(self.params.xlen // 8)) + self.spec_mem_wmask = Signal(int(self.params.xlen // 8)) + self.spec_mem_wdata = Signal(self.params.xlen) + def ports(self): input_ports = [ self.rvfi_valid, @@ -82,7 +79,7 @@ class IsaRV32I(Elaboratable): self.rvfi_rs2_rdata, self.rvfi_mem_rdata ] - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: input_ports.append(self.rvfi_csr_misa_rdata) output_ports = [ self.spec_valid, @@ -97,51 +94,52 @@ class IsaRV32I(Elaboratable): self.spec_mem_wmask, self.spec_mem_wdata ] - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: output_ports.append(self.spec_csr_misa_rmask) return input_ports + output_ports + def elaborate(self, platform): m = Module() insn_submodules = {} - m.submodules._lui = insn_submodules['lui'] = InsnLui(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._auipc = insn_submodules['auipc'] = InsnAuipc(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._jal = insn_submodules['jal'] = InsnJal(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._jalr = insn_submodules['jalr'] = InsnJalr(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._beq = insn_submodules['beq'] = InsnBeq(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._bne = insn_submodules['bne'] = InsnBne(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._blt = insn_submodules['blt'] = InsnBlt(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._bge = insn_submodules['bge'] = InsnBge(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._bltu = insn_submodules['bltu'] = InsnBltu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._bgeu = insn_submodules['bgeu'] = InsnBgeu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._lb = insn_submodules['lb'] = InsnLb(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._lh = insn_submodules['lh'] = InsnLh(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._lw = insn_submodules['lw'] = InsnLw(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._lbu = insn_submodules['lbu'] = InsnLbu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._lhu = insn_submodules['lhu'] = InsnLhu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._sb = insn_submodules['sb'] = InsnSb(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._sh = insn_submodules['Sh'] = InsnSh(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._sw = insn_submodules['sw'] = InsnSw(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED) - m.submodules._addi = insn_submodules['addi'] = InsnAddi(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._slti = insn_submodules['slti'] = InsnSlti(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._sltiu = insn_submodules['sltiu'] = InsnSltiu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._xori = insn_submodules['xori'] = InsnXori(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._ori = insn_submodules['ori'] = InsnOri(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._andi = insn_submodules['andi'] = InsnAndi(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._slli = insn_submodules['slli'] = InsnSlli(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._srli = insn_submodules['srli'] = InsnSrli(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._srai = insn_submodules['srai'] = InsnSrai(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._add = insn_submodules['add'] = InsnAdd(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._sub = insn_submodules['sub'] = InsnSub(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._sll = insn_submodules['sll'] = InsnSll(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._slt = insn_submodules['slt'] = InsnSlt(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._sltu = insn_submodules['sltu'] = InsnSltu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._xor = insn_submodules['xor'] = InsnXor(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._srl = insn_submodules['srl'] = InsnSrl(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._sra = insn_submodules['sra'] = InsnSra(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._or = insn_submodules['or'] = InsnOr(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) - m.submodules._and = insn_submodules['and'] = InsnAnd(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA) + m.submodules._lui = insn_submodules['lui'] = InsnLui(self.params) + m.submodules._auipc = insn_submodules['auipc'] = InsnAuipc(self.params) + m.submodules._jal = insn_submodules['jal'] = InsnJal(self.params) + m.submodules._jalr = insn_submodules['jalr'] = InsnJalr(self.params) + m.submodules._beq = insn_submodules['beq'] = InsnBeq(self.params) + m.submodules._bne = insn_submodules['bne'] = InsnBne(self.params) + m.submodules._blt = insn_submodules['blt'] = InsnBlt(self.params) + m.submodules._bge = insn_submodules['bge'] = InsnBge(self.params) + m.submodules._bltu = insn_submodules['bltu'] = InsnBltu(self.params) + m.submodules._bgeu = insn_submodules['bgeu'] = InsnBgeu(self.params) + m.submodules._lb = insn_submodules['lb'] = InsnLb(self.params) + m.submodules._lh = insn_submodules['lh'] = InsnLh(self.params) + m.submodules._lw = insn_submodules['lw'] = InsnLw(self.params) + m.submodules._lbu = insn_submodules['lbu'] = InsnLbu(self.params) + m.submodules._lhu = insn_submodules['lhu'] = InsnLhu(self.params) + m.submodules._sb = insn_submodules['sb'] = InsnSb(self.params) + m.submodules._sh = insn_submodules['Sh'] = InsnSh(self.params) + m.submodules._sw = insn_submodules['sw'] = InsnSw(self.params) + m.submodules._addi = insn_submodules['addi'] = InsnAddi(self.params) + m.submodules._slti = insn_submodules['slti'] = InsnSlti(self.params) + m.submodules._sltiu = insn_submodules['sltiu'] = InsnSltiu(self.params) + m.submodules._xori = insn_submodules['xori'] = InsnXori(self.params) + m.submodules._ori = insn_submodules['ori'] = InsnOri(self.params) + m.submodules._andi = insn_submodules['andi'] = InsnAndi(self.params) + m.submodules._slli = insn_submodules['slli'] = InsnSlli(self.params) + m.submodules._srli = insn_submodules['srli'] = InsnSrli(self.params) + m.submodules._srai = insn_submodules['srai'] = InsnSrai(self.params) + m.submodules._add = insn_submodules['add'] = InsnAdd(self.params) + m.submodules._sub = insn_submodules['sub'] = InsnSub(self.params) + m.submodules._sll = insn_submodules['sll'] = InsnSll(self.params) + m.submodules._slt = insn_submodules['slt'] = InsnSlt(self.params) + m.submodules._sltu = insn_submodules['sltu'] = InsnSltu(self.params) + m.submodules._xor = insn_submodules['xor'] = InsnXor(self.params) + m.submodules._srl = insn_submodules['srl'] = InsnSrl(self.params) + m.submodules._sra = insn_submodules['sra'] = InsnSra(self.params) + m.submodules._or = insn_submodules['or'] = InsnOr(self.params) + m.submodules._and = insn_submodules['and'] = InsnAnd(self.params) for _, insn in insn_submodules.items(): m.d.comb += insn.rvfi_valid.eq(self.rvfi_valid) @@ -150,7 +148,7 @@ class IsaRV32I(Elaboratable): m.d.comb += insn.rvfi_rs1_rdata.eq(self.rvfi_rs1_rdata) m.d.comb += insn.rvfi_rs2_rdata.eq(self.rvfi_rs2_rdata) m.d.comb += insn.rvfi_mem_rdata.eq(self.rvfi_mem_rdata) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += insn.rvfi_csr_misa_rdata.eq(self.rvfi_csr_misa_rdata) spec_valid = 0 @@ -208,7 +206,7 @@ class IsaRV32I(Elaboratable): spec_mem_wdata = Mux(insn.spec_valid, insn.spec_mem_wdata, spec_mem_wdata) m.d.comb += self.spec_mem_wdata.eq(spec_mem_wdata) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: spec_csr_misa_rmask = 0 for _, insn in insn_submodules.items(): spec_csr_misa_rmask = Mux(insn.spec_valid, insn.spec_csr_misa_rmask, spec_csr_misa_rmask) From d7d4f8b0add1e3861b879175eb6b88604b09e330 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Fri, 21 Aug 2020 11:43:20 +0800 Subject: [PATCH 3/4] Reduce code duplication in Minerva verification script --- rvfi/checks/causal_check.py | 2 + rvfi/checks/insn_check.py | 137 ++- rvfi/checks/pc_bwd_check.py | 16 +- rvfi/checks/pc_fwd_check.py | 16 +- rvfi/checks/reg_check.py | 16 +- rvfi/cores/minerva/verify.py | 1718 ++-------------------------------- rvfi/insns/README.md | 12 +- rvfi/insns/insn_sll.py | 2 +- rvfi/insns/insn_sra.py | 2 +- rvfi/insns/insn_srai.py | 2 +- rvfi/insns/insn_srl.py | 2 +- 11 files changed, 161 insertions(+), 1764 deletions(-) diff --git a/rvfi/checks/causal_check.py b/rvfi/checks/causal_check.py index 3e19f6a..6581589 100644 --- a/rvfi/checks/causal_check.py +++ b/rvfi/checks/causal_check.py @@ -15,6 +15,7 @@ class CausalCheck(Elaboratable): self.rvfi_order = Signal(64) self.rvfi_rs1_addr = Signal(5) self.rvfi_rs2_addr = Signal(5) + def ports(self): input_ports = [ self.reset, @@ -26,6 +27,7 @@ class CausalCheck(Elaboratable): self.rvfi_rs2_addr ] return input_ports + def elaborate(self, platform): m = Module() diff --git a/rvfi/checks/insn_check.py b/rvfi/checks/insn_check.py index 1faca58..54ad837 100644 --- a/rvfi/checks/insn_check.py +++ b/rvfi/checks/insn_check.py @@ -6,13 +6,9 @@ Instruction Check """ class InsnCheck(Elaboratable): - def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, RISCV_FORMAL_ALIGNED_MEM, insn_model, rvformal_addr_valid): - # Core-specific constants - self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN - self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA - self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED - self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM + def __init__(self, params, insn_model, rvformal_addr_valid): + # Core-specific parameters + self.params = params # Instruction under test self.insn_model = insn_model @@ -26,7 +22,7 @@ class InsnCheck(Elaboratable): self.check = Signal(1) self.rvfi_valid = Signal(1) self.rvfi_order = Signal(64) - self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN) + self.rvfi_insn = Signal(self.params.ilen) self.rvfi_trap = Signal(1) self.rvfi_halt = Signal(1) self.rvfi_intr = Signal(1) @@ -34,22 +30,23 @@ class InsnCheck(Elaboratable): self.rvfi_ixl = Signal(2) self.rvfi_rs1_addr = Signal(5) self.rvfi_rs2_addr = Signal(5) - self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rs1_rdata = Signal(self.params.xlen) + self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rd_addr = Signal(5) - self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN) - if self.RISCV_FORMAL_CSR_MISA: - self.rvfi_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_csr_misa_wmask = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_csr_misa_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rd_wdata = Signal(self.params.xlen) + self.rvfi_pc_rdata = Signal(self.params.xlen) + self.rvfi_pc_wdata = Signal(self.params.xlen) + self.rvfi_mem_addr = Signal(self.params.xlen) + self.rvfi_mem_rmask = Signal(int(self.params.xlen // 8)) + self.rvfi_mem_wmask = Signal(int(self.params.xlen // 8)) + self.rvfi_mem_rdata = Signal(self.params.xlen) + self.rvfi_mem_wdata = Signal(self.params.xlen) + if self.params.csr_misa: + self.rvfi_csr_misa_rmask = Signal(self.params.xlen) + self.rvfi_csr_misa_wmask = Signal(self.params.xlen) + self.rvfi_csr_misa_rdata = Signal(self.params.xlen) + self.rvfi_csr_misa_wdata = Signal(self.params.xlen) + def ports(self): input_ports = [ self.reset, @@ -76,7 +73,7 @@ class InsnCheck(Elaboratable): self.rvfi_mem_rdata, self.rvfi_mem_wdata ] - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: input_ports.extend([ self.rvfi_csr_misa_rmask, self.rvfi_csr_misa_wmask, @@ -84,78 +81,54 @@ class InsnCheck(Elaboratable): self.rvfi_csr_misa_wdata ]) return input_ports + def elaborate(self, platform): m = Module() valid = Signal(1) m.d.comb += valid.eq((~self.reset) & self.rvfi_valid) - insn = Signal(self.RISCV_FORMAL_ILEN) - m.d.comb += insn.eq(self.rvfi_insn) - trap = Signal(1) - m.d.comb += trap.eq(self.rvfi_trap) - halt = Signal(1) - m.d.comb += halt.eq(self.rvfi_halt) - intr = Signal(1) - m.d.comb += intr.eq(self.rvfi_intr) - rs1_addr = Signal(5) - m.d.comb += rs1_addr.eq(self.rvfi_rs1_addr) - rs2_addr = Signal(5) - m.d.comb += rs2_addr.eq(self.rvfi_rs2_addr) - rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += rs1_rdata.eq(self.rvfi_rs1_rdata) - rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += rs2_rdata.eq(self.rvfi_rs2_rdata) - rd_addr = Signal(5) - m.d.comb += rd_addr.eq(self.rvfi_rd_addr) - rd_wdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += rd_wdata.eq(self.rvfi_rd_wdata) - pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata) - pc_wdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata) + insn = self.rvfi_insn + trap = self.rvfi_trap + halt = self.rvfi_halt + intr = self.rvfi_intr + rs1_addr = self.rvfi_rs1_addr + rs2_addr = self.rvfi_rs2_addr + rs1_rdata = self.rvfi_rs1_rdata + rs2_rdata = self.rvfi_rs2_rdata + rd_addr = self.rvfi_rd_addr + rd_wdata = self.rvfi_rd_wdata + pc_rdata = self.rvfi_pc_rdata + pc_wdata = self.rvfi_pc_wdata - mem_addr = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += mem_addr.eq(self.rvfi_mem_addr) - mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - m.d.comb += mem_rmask.eq(self.rvfi_mem_rmask) - mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - m.d.comb += mem_wmask.eq(self.rvfi_mem_wmask) - mem_rdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += mem_rdata.eq(self.rvfi_mem_rdata) - mem_wdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += mem_wdata.eq(self.rvfi_mem_wdata) + mem_addr = self.rvfi_mem_addr + mem_rmask = self.rvfi_mem_rmask + mem_wmask = self.rvfi_mem_wmask + mem_rdata = self.rvfi_mem_rdata + mem_wdata = self.rvfi_mem_wdata - if self.RISCV_FORMAL_CSR_MISA: - csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += csr_misa_rdata.eq(self.rvfi_csr_misa_rdata) - csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN) - m.d.comb += csr_misa_rmask.eq(self.rvfi_csr_misa_rmask) - spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN) + if self.params.csr_misa: + csr_misa_rdata = self.rvfi_csr_misa_rdata + csr_misa_rmask = self.rvfi_csr_misa_rmask + spec_csr_misa_rmask = Signal(self.params.xlen) spec_valid = Signal(1) spec_trap = Signal(1) spec_rs1_addr = Signal(5) spec_rs2_addr = Signal(5) spec_rd_addr = Signal(5) - spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) - spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) - spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN) - spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) - spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN) + spec_rd_wdata = Signal(self.params.xlen) + spec_pc_wdata = Signal(self.params.xlen) + spec_mem_addr = Signal(self.params.xlen) + spec_mem_rmask = Signal(int(self.params.xlen // 8)) + spec_mem_wmask = Signal(int(self.params.xlen // 8)) + spec_mem_wdata = Signal(self.params.xlen) - rs1_rdata_or_zero = Signal(self.RISCV_FORMAL_XLEN) + rs1_rdata_or_zero = Signal(self.params.xlen) m.d.comb += rs1_rdata_or_zero.eq(Mux(spec_rs1_addr != 0, rs1_rdata, 0)) - rs2_rdata_or_zero = Signal(self.RISCV_FORMAL_XLEN) + rs2_rdata_or_zero = Signal(self.params.xlen) m.d.comb += rs2_rdata_or_zero.eq(Mux(spec_rs2_addr != 0, rs2_rdata, 0)) - try: - m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA) - except: - try: - m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED=self.RISCV_FORMAL_COMPRESSED) - except: - m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM=self.RISCV_FORMAL_ALIGNED_MEM) + m.submodules.insn_spec = insn_spec = self.insn_model(self.params) m.d.comb += insn_spec.rvfi_valid.eq(valid) m.d.comb += insn_spec.rvfi_insn.eq(insn) @@ -164,7 +137,7 @@ class InsnCheck(Elaboratable): m.d.comb += insn_spec.rvfi_rs2_rdata.eq(rs2_rdata_or_zero) m.d.comb += insn_spec.rvfi_mem_rdata.eq(mem_rdata) - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += insn_spec.rvfi_csr_misa_rdata.eq(csr_misa_rdata) m.d.comb += spec_csr_misa_rmask.eq(insn_spec.spec_csr_misa_rmask) @@ -208,7 +181,7 @@ class InsnCheck(Elaboratable): m.d.comb += Assert(rd_wdata == 0) m.d.comb += Assert(mem_wmask == 0) with m.Else(): - if self.RISCV_FORMAL_CSR_MISA: + if self.params.csr_misa: m.d.comb += Assert((spec_csr_misa_rmask & csr_misa_rmask) == spec_csr_misa_rmask) with m.If(rs1_addr == 0): @@ -231,7 +204,7 @@ class InsnCheck(Elaboratable): with m.If(spec_mem_wmask | spec_mem_rmask): m.d.comb += Assert(self.rvformal_addr_eq(spec_mem_addr, mem_addr)) - for i in range(int(self.RISCV_FORMAL_XLEN // 8)): + for i in range(int(self.params.xlen // 8)): with m.If(spec_mem_wmask[i]): m.d.comb += Assert(mem_wmask[i]) m.d.comb += Assert(spec_mem_wdata[i*8:i*8+8] == mem_wdata[i*8:i*8+8]) diff --git a/rvfi/checks/pc_bwd_check.py b/rvfi/checks/pc_bwd_check.py index 9c036f3..630721b 100644 --- a/rvfi/checks/pc_bwd_check.py +++ b/rvfi/checks/pc_bwd_check.py @@ -6,9 +6,9 @@ PC Backward Check """ class PcBwdCheck(Elaboratable): - def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid): - # Core-specific constants - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN + def __init__(self, params, rvformal_addr_valid): + # Core-specific parameters + self.params = params # Address validity and equality self.rvformal_addr_valid = rvformal_addr_valid @@ -19,8 +19,9 @@ class PcBwdCheck(Elaboratable): self.check = Signal(1) self.rvfi_valid = Signal(1) self.rvfi_order = Signal(64) - self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_pc_rdata = Signal(self.params.xlen) + self.rvfi_pc_wdata = Signal(self.params.xlen) + def ports(self): input_ports = [ self.reset, @@ -31,14 +32,15 @@ class PcBwdCheck(Elaboratable): self.rvfi_pc_wdata ] return input_ports + def elaborate(self, platform): m = Module() insn_order = AnyConst(64) - expect_pc = Signal(self.RISCV_FORMAL_XLEN) + expect_pc = Signal(self.params.xlen) expect_pc_valid = Signal(1, reset=0) - pc_wdata = Signal(self.RISCV_FORMAL_XLEN) + pc_wdata = Signal(self.params.xlen) m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata) with m.If(self.reset): diff --git a/rvfi/checks/pc_fwd_check.py b/rvfi/checks/pc_fwd_check.py index 8407214..3496c3e 100644 --- a/rvfi/checks/pc_fwd_check.py +++ b/rvfi/checks/pc_fwd_check.py @@ -6,9 +6,9 @@ PC Forward Check """ class PcFwdCheck(Elaboratable): - def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid): - # Core-specific constants - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN + def __init__(self, params, rvformal_addr_valid): + # Core-specific parameters + self.params = params # Address validity and equality self.rvformal_addr_valid = rvformal_addr_valid @@ -19,8 +19,9 @@ class PcFwdCheck(Elaboratable): self.check = Signal(1) self.rvfi_valid = Signal(1) self.rvfi_order = Signal(64) - self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) - self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_pc_rdata = Signal(self.params.xlen) + self.rvfi_pc_wdata = Signal(self.params.xlen) + def ports(self): input_ports = [ self.reset, @@ -31,14 +32,15 @@ class PcFwdCheck(Elaboratable): self.rvfi_pc_wdata ] return input_ports + def elaborate(self, platform): m = Module() insn_order = AnyConst(64) - expect_pc = Signal(self.RISCV_FORMAL_XLEN) + expect_pc = Signal(self.params.xlen) expect_pc_valid = Signal(1, reset=0) - pc_rdata = Signal(self.RISCV_FORMAL_XLEN) + pc_rdata = Signal(self.params.xlen) m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata) with m.If(self.reset): diff --git a/rvfi/checks/reg_check.py b/rvfi/checks/reg_check.py index 633bc25..4345028 100644 --- a/rvfi/checks/reg_check.py +++ b/rvfi/checks/reg_check.py @@ -6,9 +6,9 @@ Register Check """ class RegCheck(Elaboratable): - def __init__(self, RISCV_FORMAL_XLEN): - # Core-specific constants - self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN + def __init__(self, params): + # Core-specific parameters + self.params = params # Input ports self.reset = Signal(1) @@ -16,11 +16,12 @@ class RegCheck(Elaboratable): self.rvfi_valid = Signal(1) self.rvfi_order = Signal(64) self.rvfi_rs1_addr = Signal(5) - self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rs1_rdata = Signal(self.params.xlen) self.rvfi_rs2_addr = Signal(5) - self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rd_addr = Signal(5) - self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rd_wdata = Signal(self.params.xlen) + def ports(self): input_ports = [ self.reset, @@ -35,12 +36,13 @@ class RegCheck(Elaboratable): self.rvfi_rd_wdata ] return input_ports + def elaborate(self, platform): m = Module() insn_order = AnyConst(64) register_index = AnyConst(5) - register_shadow = Signal(self.RISCV_FORMAL_XLEN, reset=0) + register_shadow = Signal(self.params.xlen, reset=0) register_written = Signal(1, reset=0) with m.If(self.reset): diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index fe3563a..792301c 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -1,5 +1,3 @@ -import sys -import traceback from nmigen.test.utils import * from ...checks.insn_check import * from ...checks.pc_fwd_check import * @@ -44,21 +42,19 @@ from ...insns.insn_srl import * from ...insns.insn_sra import * from ...insns.insn_or import * from ...insns.insn_and import * +from ...riscv_formal_parameters import * -stderr = sys.stderr -sys.stderr = open('/dev/null', 'w') +class InsnSpec(Elaboratable): + def __init__(self, insn_model): + self.insn_model = insn_model -class LuiSpec(Elaboratable): def elaborate(self, platform): m = Module() m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLui, + m.submodules.insn_spec = insn_spec = InsnCheck( + params=RISCVFormalParameters(32, 32, False, False, False), + insn_model=self.insn_model, rvformal_addr_valid=lambda x:Const(1)) m.d.comb += insn_spec.reset.eq(0) @@ -88,1600 +84,59 @@ class LuiSpec(Elaboratable): return m -class LuiTestCase(FHDLTestCase): +class InsnTestCase(FHDLTestCase): def verify(self): - self.assertFormal(LuiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class AuipcSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnAuipc, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class AuipcTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(AuipcSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class JalSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnJal, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class JalTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(JalSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class JalrSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnJalr, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class JalrTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(JalrSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BeqSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBeq, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BeqTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BeqSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BneSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBne, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BneTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BneSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BltSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBlt, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BltTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BltSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BgeSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBge, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BgeTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BgeSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BltuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBltu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BltuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BltuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class BgeuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnBgeu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class BgeuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(BgeuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class LbSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLb, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class LbTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(LbSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class LhSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLh, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class LhTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(LhSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class LwSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLw, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class LwTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(LwSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class LbuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLbu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class LbuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(LbuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class LhuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnLhu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class LhuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(LhuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SbSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSb, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SbTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SbSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class ShSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSh, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class ShTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(ShSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SwSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSw, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SwTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SwSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class AddiSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnAddi, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class AddiTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(AddiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SltiSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSlti, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SltiTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SltiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SltiuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSltiu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SltiuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SltiuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class XoriSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnXori, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class XoriTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(XoriSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class OriSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnOri, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class OriTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(OriSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class AndiSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnAndi, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class AndiTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(AndiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SlliSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSlli, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SlliTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SlliSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SrliSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSrli, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SrliTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SrliSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SraiSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSrai, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SraiTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SraiSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class AddSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnAdd, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class AddTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(AddSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SubSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSub, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SubTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SubSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SllSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSll, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SllTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SllSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SltSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSlt, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SltTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SltSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SltuSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSltu, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SltuTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SltuSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class XorSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnXor, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class XorTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(XorSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SrlSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSrl, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SrlTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SrlSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class SraSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnSra, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class SraTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(SraSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class OrSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnOr, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class OrTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(OrSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") - -class AndSpec(Elaboratable): - def elaborate(self, platform): - m = Module() - - m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.insn_spec = insn_spec = InsnCheck(RISCV_FORMAL_ILEN=32, - RISCV_FORMAL_XLEN=32, - RISCV_FORMAL_CSR_MISA=False, - RISCV_FORMAL_COMPRESSED=False, - RISCV_FORMAL_ALIGNED_MEM=False, - insn_model=InsnAnd, - rvformal_addr_valid=lambda x:Const(1)) - - m.d.comb += insn_spec.reset.eq(0) - m.d.comb += insn_spec.check.eq(1) - - m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid) - m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order) - m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn) - m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap) - m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt) - m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr) - m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode) - m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl) - m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr) - m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr) - m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata) - m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata) - m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr) - m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata) - m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) - m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) - m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr) - m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask) - m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask) - m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata) - m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata) - - return m - -class AndTestCase(FHDLTestCase): - def verify(self): - self.assertFormal(AndSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") + insns = [ + ('LUI', InsnLui), + ('AUIPC', InsnAuipc), + ('JAL', InsnJal), + ('JALR', InsnJalr), + ('BEQ', InsnBeq), + ('BNE', InsnBne), + ('BLT', InsnBlt), + ('BGE', InsnBge), + ('BLTU', InsnBltu), + ('BGEU', InsnBgeu), + ('LB', InsnLb), + ('LH', InsnLh), + ('LW', InsnLw), + ('LBU', InsnLbu), + ('LHU', InsnLhu), + ('SB', InsnSb), + ('SH', InsnSh), + ('SW', InsnSw), + ('ADDI', InsnAddi), + ('SLTI', InsnSlti), + ('SLTIU', InsnSltiu), + ('XORI', InsnXori), + ('ORI', InsnOri), + ('ANDI', InsnAndi), + ('SLLI', InsnSlli), + ('SRLI', InsnSrli), + ('SRAI', InsnSrai), + ('ADD', InsnAdd), + ('SUB', InsnSub), + ('SLL', InsnSll), + ('SLT', InsnSlt), + ('SLTU', InsnSltu), + ('XOR', InsnXor), + ('SRL', InsnSrl), + ('SRA', InsnSra), + ('OR', InsnOr), + ('AND', InsnAnd) + ] + for insn_name, insn_model in insns: + print("- Verifying instruction %s ..." % insn_name) + self.assertFormal(InsnSpec(insn_model), mode="bmc", depth=12, engine="smtbmc --nopresat") class PcFwdSpec(Elaboratable): def elaborate(self, platform): m = Module() m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(1)) + m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck( + params=RISCVFormalParameters(32, 32, False, False, False), + rvformal_addr_valid=lambda x:Const(1)) m.d.comb += pc_fwd_spec.reset.eq(0) m.d.comb += pc_fwd_spec.check.eq(1) @@ -1702,7 +157,9 @@ class PcBwdSpec(Elaboratable): m = Module() m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(1)) + m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck( + params=RISCVFormalParameters(32, 32, False, False, False), + rvformal_addr_valid=lambda x:Const(1)) m.d.comb += pc_bwd_spec.reset.eq(0) m.d.comb += pc_bwd_spec.check.eq(1) @@ -1723,7 +180,7 @@ class RegSpec(Elaboratable): m = Module() m.submodules.cpu = cpu = Minerva(with_rvfi=True) - m.submodules.reg_spec = reg_spec = RegCheck(RISCV_FORMAL_XLEN=32) + m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False)) m.d.comb += reg_spec.reset.eq(0) m.d.comb += reg_spec.check.eq(1) @@ -1769,61 +226,20 @@ print('* Verifying the Minerva core ... print('*' + ' ' * 78 + '*') print('*' * 80) -try: - print("Verifying RV32I instructions ...") - LuiTestCase().verify() - AuipcTestCase().verify() - JalTestCase().verify() - JalrTestCase().verify() - BeqTestCase().verify() - BneTestCase().verify() - BltTestCase().verify() - BgeTestCase().verify() - BltuTestCase().verify() - BgeuTestCase().verify() - LbTestCase().verify() - LhTestCase().verify() - LwTestCase().verify() - LbuTestCase().verify() - LhuTestCase().verify() - SbTestCase().verify() - ShTestCase().verify() - SwTestCase().verify() - AddiTestCase().verify() - SltiTestCase().verify() - SltiuTestCase().verify() - XoriTestCase().verify() - OriTestCase().verify() - AndiTestCase().verify() - SlliTestCase().verify() - SrliTestCase().verify() - SraiTestCase().verify() - AddTestCase().verify() - SubTestCase().verify() - SllTestCase().verify() - SltTestCase().verify() - SltuTestCase().verify() - XorTestCase().verify() - SrlTestCase().verify() - SraTestCase().verify() - OrTestCase().verify() - AndTestCase().verify() +print("Verifying RV32I instructions ...") +InsnTestCase().verify() - print("Verifying PC forward checks ...") - PcFwdTestCase().verify() +print("Verifying PC forward checks ...") +PcFwdTestCase().verify() - print("Verifying PC backward checks ...") - PcBwdTestCase().verify() +print("Verifying PC backward checks ...") +PcBwdTestCase().verify() - print("Verifying register checks ...") - RegTestCase().verify() +print("Verifying register checks ...") +RegTestCase().verify() - print("Verifying causal checks ...") - CausalTestCase().verify() -except: - sys.stderr = stderr - traceback.print_exc() - sys.exit(1) +print("Verifying causal checks ...") +CausalTestCase().verify() print('*' * 80) print('*' + ' ' * 78 + '*') diff --git a/rvfi/insns/README.md b/rvfi/insns/README.md index 00e3768..13960ff 100644 --- a/rvfi/insns/README.md +++ b/rvfi/insns/README.md @@ -93,10 +93,10 @@ Below is a list of instructions currently supported by this port of the riscv-fo The following core-specific parameters are currently supported: -| Constant | Description | Valid value(s) | +| Parameter | Description | Valid value(s) | | --- | --- | --- | -| `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | -| `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | -| `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | -| `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | -| `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | +| `params.ilen` | Max length of instruction retired by core | `32` | +| `params.xlen` | Width of integer registers | `32` | +| `params.csr_misa` | Support for MISA CSRs enabled | `True`, `False` | +| `params.compressed` | Support for compressed instructions | `True`, `False` | +| `params.aligned_mem` | Require aligned memory accesses | `True`, `False` | diff --git a/rvfi/insns/insn_sll.py b/rvfi/insns/insn_sll.py index 9263fe5..1897bd3 100644 --- a/rvfi/insns/insn_sll.py +++ b/rvfi/insns/insn_sll.py @@ -11,6 +11,6 @@ class InsnSll(InsnRV32IRType): def elaborate(self, platform): m = super().elaborate(platform) - m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) + m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) return m diff --git a/rvfi/insns/insn_sra.py b/rvfi/insns/insn_sra.py index 6cbc76a..71a4d87 100644 --- a/rvfi/insns/insn_sra.py +++ b/rvfi/insns/insn_sra.py @@ -11,6 +11,6 @@ class InsnSra(InsnRV32IRType): def elaborate(self, platform): m = super().elaborate(platform) - m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5])) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]))), 0)) # https://stackoverflow.com/a/25207042 + m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5])) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.params.xlen - Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]))), 0)) # https://stackoverflow.com/a/25207042 return m diff --git a/rvfi/insns/insn_srai.py b/rvfi/insns/insn_srai.py index 1e1f6a4..f9b6390 100644 --- a/rvfi/insns/insn_srai.py +++ b/rvfi/insns/insn_srai.py @@ -11,6 +11,6 @@ class InsnSrai(InsnRV32IITypeShift): def elaborate(self, platform): m = super().elaborate(platform) - m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> self.insn_shamt) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - self.insn_shamt)), 0)) + m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> self.insn_shamt) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.params.xlen - self.insn_shamt)), 0)) return m diff --git a/rvfi/insns/insn_srl.py b/rvfi/insns/insn_srl.py index 4f2d2f9..1f95471 100644 --- a/rvfi/insns/insn_srl.py +++ b/rvfi/insns/insn_srl.py @@ -11,6 +11,6 @@ class InsnSrl(InsnRV32IRType): def elaborate(self, platform): m = super().elaborate(platform) - m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) + m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) return m From c6b9bb9a04471156956732d0fc320b567605e0f0 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Fri, 21 Aug 2020 11:46:39 +0800 Subject: [PATCH 4/4] Update README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 46b072d..5fd9232 100644 --- a/README.md +++ b/README.md @@ -4,14 +4,14 @@ A port of [riscv-formal](https://github.com/SymbioticEDA/riscv-formal) to nMigen ## Breakdown -| Directory | Description | +| File/Directory | Description | | --- | --- | | `shell.nix` | [nix-shell](https://nixos.wiki/wiki/Development_environment_with_nix-shell) configuration file | | `rvfi` | RISC-V Formal Verification Framework (nMigen port) | | `rvfi/insns` | Supported RISC-V instructions and ISAs | | `rvfi/checks` | Checks for RISC-V compliant cores | | `rvfi/cores` | Cores currently tested against this port of riscv-formal | -| `rvfi/cores/minerva` | Tests for the Minerva core | +| `rvfi/cores/minerva/verify.py` | Verification tasks for the Minerva core | ## Running the Verification