From 2a4f6dd07ee7769796dac7adbe9530f3c67f7a1f Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Mon, 24 Aug 2020 13:28:33 +0800
Subject: [PATCH] Wire interrupt signals to Minerva for verification
---
rvfi/cores/minerva/verify.py | 63 ++++++++++++++++++++++++++++++++++++
1 file changed, 63 insertions(+)
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index bf07d8d..5eb1ff9 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -26,6 +26,15 @@ class InsnSpec(Elaboratable):
insn_model=self.insn_model,
rvformal_addr_valid=lambda x:Const(1))
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += insn_spec.reset.eq(0)
m.d.comb += insn_spec.check.eq(1)
@@ -66,6 +75,15 @@ class PcFwdSpec(Elaboratable):
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += pc_fwd_spec.reset.eq(0)
m.d.comb += pc_fwd_spec.check.eq(1)
@@ -89,6 +107,15 @@ class PcBwdSpec(Elaboratable):
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += pc_bwd_spec.reset.eq(0)
m.d.comb += pc_bwd_spec.check.eq(1)
@@ -110,6 +137,15 @@ class RegSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False))
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
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)
@@ -134,6 +170,15 @@ class CausalSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.causal_spec = causal_spec = CausalCheck()
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += causal_spec.reset.eq(0)
m.d.comb += causal_spec.check.eq(1)
m.d.comb += causal_spec.rvfi_valid.eq(cpu.rvfi.valid)
@@ -155,6 +200,15 @@ class LivenessSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.liveness_spec = liveness_spec = LivenessCheck()
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += liveness_spec.reset.eq(0)
m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
@@ -175,6 +229,15 @@ class UniqueSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.unique_spec = unique_spec = UniqueCheck()
+ # Connect Wishbone instruction bus to Minerva CPU
+ # TODO
+ # Connect Wishbone data bus to Minerva CPU
+ # TODO
+ # Disable all interrupts
+ m.d.comb += cpu.external_interrupt.eq(0)
+ m.d.comb += cpu.timer_interrupt.eq(0)
+ m.d.comb += cpu.software_interrupt.eq(0)
+
m.d.comb += unique_spec.reset.eq(0)
m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)