From d7d4f8b0add1e3861b879175eb6b88604b09e330 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Fri, 21 Aug 2020 11:43:20 +0800 Subject: [PATCH] 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