From 2a9ddf0868266a31dcf5aeae05855f10d5d72461 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Thu, 20 Aug 2020 11:10:33 +0800
Subject: [PATCH] Add register checks
---
rvfi/checks/reg_check.py | 62 ++++++++++++++++++++++++
rvfi/cores/minerva/test/test_register.py | 28 +++++++++++
rvfi/cores/minerva/verify.py | 4 ++
3 files changed, 94 insertions(+)
create mode 100644 rvfi/checks/reg_check.py
create mode 100644 rvfi/cores/minerva/test/test_register.py
diff --git a/rvfi/checks/reg_check.py b/rvfi/checks/reg_check.py
new file mode 100644
index 0000000..633bc25
--- /dev/null
+++ b/rvfi/checks/reg_check.py
@@ -0,0 +1,62 @@
+from nmigen import *
+from nmigen.asserts import *
+
+"""
+Register Check
+"""
+
+class RegCheck(Elaboratable):
+ def __init__(self, RISCV_FORMAL_XLEN):
+ # Core-specific constants
+ self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
+
+ # Input ports
+ self.reset = Signal(1)
+ self.check = Signal(1)
+ 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_rs2_addr = Signal(5)
+ self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
+ self.rvfi_rd_addr = Signal(5)
+ self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
+ def ports(self):
+ input_ports = [
+ self.reset,
+ self.check,
+ self.rvfi_valid,
+ self.rvfi_order,
+ self.rvfi_rs1_addr,
+ self.rvfi_rs1_rdata,
+ self.rvfi_rs2_addr,
+ self.rvfi_rs2_rdata,
+ self.rvfi_rd_addr,
+ 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_written = Signal(1, reset=0)
+
+ with m.If(self.reset):
+ m.d.sync += register_shadow.eq(0)
+ m.d.sync += register_written.eq(0)
+ with m.Else():
+ with m.If(self.check):
+ m.d.comb += Assume(self.rvfi_valid)
+ m.d.comb += Assume(insn_order == self.rvfi_order)
+ with m.If(register_written & (register_index == self.rvfi_rs1_addr)):
+ m.d.comb += Assert(register_shadow == self.rvfi_rs1_rdata)
+ with m.If(register_written & (register_index == self.rvfi_rs2_addr)):
+ m.d.comb += Assert(register_shadow == self.rvfi_rs2_rdata)
+ with m.Else():
+ with m.If(self.rvfi_valid & (self.rvfi_order < insn_order) & (register_index == self.rvfi_rd_addr)):
+ m.d.sync += register_shadow.eq(self.rvfi_rd_wdata)
+ m.d.sync += register_written.eq(1)
+
+ return m
diff --git a/rvfi/cores/minerva/test/test_register.py b/rvfi/cores/minerva/test/test_register.py
new file mode 100644
index 0000000..067ffac
--- /dev/null
+++ b/rvfi/cores/minerva/test/test_register.py
@@ -0,0 +1,28 @@
+from nmigen import *
+from ..core import *
+from nmigen.test.utils import *
+from ....checks.reg_check import *
+
+class RegSpec(Elaboratable):
+ def elaborate(self, platform):
+ m = Module()
+
+ m.submodules.cpu = cpu = Minerva(with_rvfi=True)
+ m.submodules.reg_spec = reg_spec = RegCheck(RISCV_FORMAL_XLEN=32)
+
+ m.d.comb += reg_spec.reset.eq(0)
+ m.d.comb += reg_spec.check.eq(1)
+ m.d.comb += reg_spec.rvfi_valid.eq(cpu.rvfi.valid)
+ m.d.comb += reg_spec.rvfi_order.eq(cpu.rvfi.order)
+ m.d.comb += reg_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
+ m.d.comb += reg_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
+ m.d.comb += reg_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
+ m.d.comb += reg_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
+ m.d.comb += reg_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
+ m.d.comb += reg_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)
+
+ return m
+
+class RegTestCase(FHDLTestCase):
+ def verify(self):
+ self.assertFormal(RegSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index b7c626f..44279bc 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -3,6 +3,7 @@ from .test.test_cache import *
from .test.test_instructions import *
from .test.test_pc_forward import *
from .test.test_pc_backward import *
+from .test.test_register import *
from .test.test_units_divider import *
from .test.test_units_multiplier import *
@@ -56,5 +57,8 @@ PcFwdTestCase().verify()
print("Verifying PC backward checks ...")
PcBwdTestCase().verify()
+print("Verifying register checks ...")
+RegTestCase().verify()
+
print("Testing multiplier and divider ...")
unittest.main()