From 2bfd909b49a572def15fcc7c810566510bc886f0 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Wed, 19 Aug 2020 17:00:11 +0800
Subject: [PATCH] Add PC forward checks
---
rvfi/checks/pc_fwd_check.py | 57 ++++++++++++++++++++++
rvfi/cores/minerva/test/test_pc_forward.py | 25 ++++++++++
rvfi/cores/minerva/verify.py | 4 ++
3 files changed, 86 insertions(+)
create mode 100644 rvfi/checks/pc_fwd_check.py
create mode 100644 rvfi/cores/minerva/test/test_pc_forward.py
diff --git a/rvfi/checks/pc_fwd_check.py b/rvfi/checks/pc_fwd_check.py
new file mode 100644
index 0000000..8407214
--- /dev/null
+++ b/rvfi/checks/pc_fwd_check.py
@@ -0,0 +1,57 @@
+from nmigen import *
+from nmigen.asserts import *
+
+"""
+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
+
+ # Address validity and equality
+ self.rvformal_addr_valid = rvformal_addr_valid
+ self.rvformal_addr_eq = lambda a, b: (self.rvformal_addr_valid(a) == self.rvformal_addr_valid(b)) & ((~self.rvformal_addr_valid(a)) | (a == b))
+
+ # Input ports
+ self.reset = Signal(1)
+ 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)
+ def ports(self):
+ input_ports = [
+ self.reset,
+ self.check,
+ self.rvfi_valid,
+ self.rvfi_order,
+ self.rvfi_pc_rdata,
+ 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_valid = Signal(1, reset=0)
+
+ pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
+ m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
+
+ with m.If(self.reset):
+ m.d.sync += expect_pc_valid.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(expect_pc_valid):
+ m.d.comb += Assert(self.rvformal_addr_eq(expect_pc, pc_rdata))
+ with m.Else():
+ with m.If(self.rvfi_valid & (self.rvfi_order == insn_order - 1)):
+ m.d.sync += expect_pc.eq(self.rvfi_pc_wdata)
+ m.d.sync += expect_pc_valid.eq(1)
+
+ return m
diff --git a/rvfi/cores/minerva/test/test_pc_forward.py b/rvfi/cores/minerva/test/test_pc_forward.py
new file mode 100644
index 0000000..d43cf0c
--- /dev/null
+++ b/rvfi/cores/minerva/test/test_pc_forward.py
@@ -0,0 +1,25 @@
+from nmigen import *
+from nmigen.test.utils import *
+from ..core import *
+from ....checks.pc_fwd_check import *
+
+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.d.comb += pc_fwd_spec.reset.eq(0)
+ m.d.comb += pc_fwd_spec.check.eq(1)
+
+ m.d.comb += pc_fwd_spec.rvfi_valid.eq(cpu.rvfi.valid)
+ m.d.comb += pc_fwd_spec.rvfi_order.eq(cpu.rvfi.order)
+ m.d.comb += pc_fwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
+ m.d.comb += pc_fwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)
+
+ return m
+
+class PcFwdTestCase(FHDLTestCase):
+ def verify(self):
+ self.assertFormal(PcFwdSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat")
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index 9c4fcca..fe18bd7 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -1,6 +1,7 @@
import unittest
from .test.test_cache import *
from .test.test_instructions import *
+from .test.test_pc_forward import *
from .test.test_units_divider import *
from .test.test_units_multiplier import *
@@ -48,5 +49,8 @@ SraTestCase().verify()
OrTestCase().verify()
AndTestCase().verify()
+print("Verifying PC forward checks ...")
+PcFwdTestCase().verify()
+
print("Testing multiplier and divider ...")
unittest.main()