From 0e0d4b6e4262bfbf42abc58fada280b0804b3a7b Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Tue, 18 Aug 2020 14:10:47 +0800
Subject: [PATCH] Add (currently failing) test case for LUI instruction
---
rvfi/cores/minerva/test/test_instructions.py | 49 ++++++++++++++++++++
rvfi/cores/minerva/verify.py | 7 +++
2 files changed, 56 insertions(+)
create mode 100644 rvfi/cores/minerva/test/test_instructions.py
diff --git a/rvfi/cores/minerva/test/test_instructions.py b/rvfi/cores/minerva/test/test_instructions.py
new file mode 100644
index 0000000..4d8c9ac
--- /dev/null
+++ b/rvfi/cores/minerva/test/test_instructions.py
@@ -0,0 +1,49 @@
+from nmigen import *
+from nmigen.test.utils import *
+from ..core import *
+from ....checks.insn_check import *
+from ....insns.insn_lui import *
+
+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,
+ 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 LuiTestCase(FHDLTestCase):
+ def verify(self):
+ self.assertFormal(LuiSpec(), mode="bmc", depth=12)
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index 6db55d9..8663aea 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -1,9 +1,16 @@
import unittest
from .test.test_cache import *
+from .test.test_instructions import *
from .test.test_units_divider import *
from .test.test_units_multiplier import *
+print("Verifying L1 cache ...")
test = L1CacheTestCase()
test.test_direct_mapped()
test.test_2_ways()
+
+print("Verifying RV32I instructions ...")
+LuiTestCase().verify()
+
+print("Testing multiplier and divider ...")
unittest.main()