Merge instruction and data bus abstractions

rvfi/cores/minerva/ibus.py

@@ -1,45 +0,0 @@
-from nmigen import *
-
-"""
-Instruction Bus (Wishbone Slave)
-"""
-
-# TODO: Perhaps axiomatize a read-only instruction store where the
-# instruction bus reads from when requested by the CPU core?
-
-class InstructionBus(Elaboratable):
-    def __init__(self):
-        self.adr = Signal(30)
-        self.dat_w = Signal(32)
-        self.dat_r = Signal(32)
-        self.sel = Signal(4)
-        self.cyc = Signal(1)
-        self.stb = Signal(1)
-        self.ack = Signal(1)
-        self.we = Signal(1)
-        self.cti = Signal(3)
-        self.bte = Signal(2)
-        self.err = Signal(1)
-    def ports(self):
-        input_ports = [
-            self.adr,
-            self.dat_w,
-            self.sel,
-            self.cyc,
-            self.stb,
-            self.we,
-            self.cti,
-            self.bte
-        ]
-        output_ports = [
-            self.dat_r,
-            self.ack,
-            self.err
-        ]
-        return input_ports + output_ports
-    def elaborate(self, platform):
-        m = Module()
-
-        # TODO
-
-        return m

rvfi/cores/minerva/memory_bus.py

@@ -1,13 +1,10 @@
 from nmigen import *
 
 """
-Data Bus (Wishbone Slave)
+Memory Bus (Wishbone Slave)
 """
 
-# TODO: Perhaps axiomatize a read-write data store where the
+class MemoryBus(Elaboratable):
-# data bus reads from / writes to when requested by the CPU core?
-
-class DataBus(Elaboratable):
     def __init__(self):
         self.adr = Signal(30)
         self.dat_w = Signal(32)

rvfi/cores/minerva/verify.py

@@ -8,8 +8,7 @@ from ...checks.liveness_check import *
 from ...checks.unique_check import *
 from minerva.core import *
 from ...insns.isa_rv32i import *
-from .ibus import *
+from .memory_bus import *
-from .dbus import *
 from collections import namedtuple
 
 RISCVFormalParameters = namedtuple('RISCVFormalParameters',
@@ -29,7 +28,7 @@ class InsnSpec(Elaboratable):
             rvformal_addr_valid=lambda x:Const(1))
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -42,7 +41,7 @@ class InsnSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -100,7 +99,7 @@ class PcFwdSpec(Elaboratable):
             rvformal_addr_valid=lambda x:Const(1))
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -113,7 +112,7 @@ class PcFwdSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -154,7 +153,7 @@ class PcBwdSpec(Elaboratable):
             rvformal_addr_valid=lambda x:Const(1))
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -167,7 +166,7 @@ class PcBwdSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -206,7 +205,7 @@ class RegSpec(Elaboratable):
         m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False))
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -219,7 +218,7 @@ class RegSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -261,7 +260,7 @@ class CausalSpec(Elaboratable):
         m.submodules.causal_spec = causal_spec = CausalCheck()
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -274,7 +273,7 @@ class CausalSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -313,7 +312,7 @@ class LivenessSpec(Elaboratable):
         m.submodules.liveness_spec = liveness_spec = LivenessCheck()
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -326,7 +325,7 @@ class LivenessSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
@@ -364,7 +363,7 @@ class UniqueSpec(Elaboratable):
         m.submodules.unique_spec = unique_spec = UniqueCheck()
 
         # Connect Wishbone instruction bus to Minerva CPU
-        m.submodules.ibus = ibus = InstructionBus()
+        m.submodules.ibus = ibus = MemoryBus()
         m.d.comb += ibus.adr.eq(cpu.ibus.adr)
         m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
         m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
@@ -377,7 +376,7 @@ class UniqueSpec(Elaboratable):
         m.d.comb += ibus.bte.eq(cpu.ibus.bte)
         m.d.comb += cpu.ibus.err.eq(ibus.err)
         # Connect Wishbone data bus to Minerva CPU
-        m.submodules.dbus = dbus = DataBus()
+        m.submodules.dbus = dbus = MemoryBus()
         m.d.comb += dbus.adr.eq(cpu.dbus.adr)
         m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
         m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)