109 lines
4.2 KiB
Python
109 lines
4.2 KiB
Python
from nmigen import *
|
|
from nmigen.asserts import *
|
|
|
|
"""
|
|
Memory Bus (Wishbone Slave)
|
|
"""
|
|
|
|
class MemoryBus(Elaboratable):
|
|
def __init__(self):
|
|
# Input/output ports
|
|
self.adr = Signal(30)
|
|
self.dat_w = Signal(32)
|
|
self.dat_r = Signal(32)
|
|
self.sel = Signal(4) # ignored during reads, just return the whole word
|
|
self.cyc = Signal(1)
|
|
self.stb = Signal(1)
|
|
self.ack = Signal(1, reset=0)
|
|
self.we = Signal(1)
|
|
self.cti = Signal(3) # ignored (signal for performance purposes only?)
|
|
self.bte = Signal(2) # ignored (signal for performance purposes only?)
|
|
self.err = Const(0) # unsupported
|
|
|
|
# Memory store
|
|
self.memory = Array(AnySeq(32) for _ in range(1 << 30))
|
|
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()
|
|
|
|
# Indicator of when Past() is valid
|
|
f_past_valid = Signal(1, reset=0)
|
|
m.d.sync += f_past_valid.eq(1)
|
|
|
|
# Memory store in the past clock cycle
|
|
f_past_memory = Array(Signal(32) for _ in range(1 << 30))
|
|
for i in range(1 << 30):
|
|
m.d.sync += f_past_memory[i].eq(self.memory[i])
|
|
|
|
# Unless both cyc and stb are asserted:
|
|
# - ack should be de-asserted on the next clock edge
|
|
# - memory contents should remain constant
|
|
with m.If(~self.cyc | ~self.stb):
|
|
m.d.sync += ack.eq(0)
|
|
with m.If(f_past_valid & ((~Past(self.cyc)) | ~Past(self.stb))):
|
|
for i in range(1 << 30):
|
|
m.d.comb += Assume(self.memory[i] == f_past_memory[i])
|
|
|
|
# If cyc, stb are asserted and ack de-asserted:
|
|
# - For a read (i.e. WE is de-asserted):
|
|
# - dat_r should contain the word under the given address at the
|
|
# next clock cycle
|
|
# - ack should be asserted in the next clock cycle
|
|
# - memory contents should remain constant
|
|
with m.If(self.cyc & self.stb & ~self.ack):
|
|
with m.If(~self.we):
|
|
m.d.sync += self.dat_r.eq(self.memory[self.adr])
|
|
m.d.sync += self.ack.eq(1)
|
|
with m.If(f_past_valid & Past(self.cyc) & Past(self.stb) & ~Past(self.ack)):
|
|
with m.If(~Past(self.we)):
|
|
for i in range(1 << 30):
|
|
m.d.comb += Assume(self.memory[i] == f_past_memory[i])
|
|
# - For a write (i.e. WE is asserted)
|
|
# - ack should be asserted in the next clock cycle
|
|
# - For the word of data under adr:
|
|
# - If the select bit is asserted, the corresponding byte is
|
|
# written to memory
|
|
# - Otherwise, the corresponding byte remains constant
|
|
# - All other memory content should remain constant
|
|
with m.If(self.cyc & self.stb & ~self.ack):
|
|
with m.If(self.we):
|
|
m.d.sync += self.ack.eq(1)
|
|
with m.If(f_past_valid & Past(self.cyc) & Past(self.stb) & ~Past(self.ack)):
|
|
with m.If(Past(self.we)):
|
|
for i in range(1 << 30):
|
|
with m.If(i == Past(self.adr)):
|
|
for j in range(4):
|
|
with m.If(Past(self.sel)[j]):
|
|
m.d.comb += Assume(self.memory[i][j*8:j*8+8] == Past(self.dat_w)[j*8:j*8+8])
|
|
with m.Else():
|
|
m.d.comb += Assume(self.memory[i][j*8:j*8+8] == f_past_memory[i][j*8:j*8+8])
|
|
with m.Else():
|
|
m.d.comb += Assume(self.memory[i] == f_past_memory[i])
|
|
|
|
# If ack is asserted:
|
|
# - ack should be de-asserted in the next clock cycle
|
|
# - memory contents should remain constant
|
|
with m.If(self.ack):
|
|
m.d.sync += self.ack.eq(0)
|
|
with m.If(f_past_valid & Past(self.ack)):
|
|
for i in range(1 << 30):
|
|
m.d.comb += Assume(self.memory[i] == f_past_memory[i])
|
|
|
|
return m
|