diff --git a/rvfi/cores/minerva/ibus.py b/rvfi/cores/minerva/ibus.py deleted file mode 100644 index 0e6e676..0000000 --- a/rvfi/cores/minerva/ibus.py +++ /dev/null @@ -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 diff --git a/rvfi/cores/minerva/dbus.py b/rvfi/cores/minerva/memory_bus.py similarity index 82% rename from rvfi/cores/minerva/dbus.py rename to rvfi/cores/minerva/memory_bus.py index 829b42d..7b47cf6 100644 --- a/rvfi/cores/minerva/dbus.py +++ b/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 -# data bus reads from / writes to when requested by the CPU core? - -class DataBus(Elaboratable): +class MemoryBus(Elaboratable): def __init__(self): self.adr = Signal(30) self.dat_w = Signal(32) diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index bdd1070..3472da0 100644 --- a/rvfi/cores/minerva/verify.py +++ b/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 .dbus import * +from .memory_bus 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)