diff --git a/rvfi/cores/minerva/dbus.py b/rvfi/cores/minerva/dbus.py new file mode 100644 index 0000000..829b42d --- /dev/null +++ b/rvfi/cores/minerva/dbus.py @@ -0,0 +1,45 @@ +from nmigen import * + +""" +Data 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): + 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/ibus.py b/rvfi/cores/minerva/ibus.py new file mode 100644 index 0000000..0e6e676 --- /dev/null +++ b/rvfi/cores/minerva/ibus.py @@ -0,0 +1,45 @@ +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/verify.py b/rvfi/cores/minerva/verify.py index 5eb1ff9..bdd1070 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -8,6 +8,8 @@ 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 collections import namedtuple RISCVFormalParameters = namedtuple('RISCVFormalParameters', @@ -27,9 +29,31 @@ class InsnSpec(Elaboratable): rvformal_addr_valid=lambda x:Const(1)) # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -76,9 +100,31 @@ class PcFwdSpec(Elaboratable): rvformal_addr_valid=lambda x:Const(1)) # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -108,9 +154,31 @@ class PcBwdSpec(Elaboratable): rvformal_addr_valid=lambda x:Const(1)) # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -138,9 +206,31 @@ class RegSpec(Elaboratable): m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False)) # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -171,9 +261,31 @@ class CausalSpec(Elaboratable): m.submodules.causal_spec = causal_spec = CausalCheck() # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -201,9 +313,31 @@ class LivenessSpec(Elaboratable): m.submodules.liveness_spec = liveness_spec = LivenessCheck() # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0) @@ -230,9 +364,31 @@ class UniqueSpec(Elaboratable): m.submodules.unique_spec = unique_spec = UniqueCheck() # Connect Wishbone instruction bus to Minerva CPU - # TODO + m.submodules.ibus = ibus = InstructionBus() + 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) + m.d.comb += ibus.sel.eq(cpu.ibus.sel) + m.d.comb += ibus.cyc.eq(cpu.ibus.cyc) + m.d.comb += ibus.stb.eq(cpu.ibus.stb) + m.d.comb += cpu.ibus.ack.eq(ibus.ack) + m.d.comb += ibus.we.eq(cpu.ibus.we) + m.d.comb += ibus.cti.eq(cpu.ibus.cti) + 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 - # TODO + m.submodules.dbus = dbus = DataBus() + 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) + m.d.comb += dbus.sel.eq(cpu.dbus.sel) + m.d.comb += dbus.cyc.eq(cpu.dbus.cyc) + m.d.comb += dbus.stb.eq(cpu.dbus.stb) + m.d.comb += cpu.dbus.ack.eq(dbus.ack) + m.d.comb += dbus.we.eq(cpu.dbus.we) + m.d.comb += dbus.cti.eq(cpu.dbus.cti) + m.d.comb += dbus.bte.eq(cpu.dbus.bte) + m.d.comb += cpu.dbus.err.eq(dbus.err) # Disable all interrupts m.d.comb += cpu.external_interrupt.eq(0) m.d.comb += cpu.timer_interrupt.eq(0)