Add prototype for instruction/data bus implementation

README.md

@@ -35,7 +35,10 @@ Support for the RV32I base ISA and RV32M extension are planned and well underway
 
 ## Known Issues
 
-As of 21/08/2020, the verification passes unconditionally, even when obvious, deliberate bugs are introduced to the Minerva core and/or its components thereof (such as replacing subtraction with addition in the adder). This is caused by the Minerva core having its `rvfi.valid` signal de-asserted all of the time. The cause of this issue is very likely due to the absence of proper interrupt signals and instruction + data buses, which must be connected to the core for it to function properly. Perhaps the issue could be solved by constructing abstract instruction + data buses with suitable assumed properties and connecting those abstract interfaces to the Minerva core (but then, what would those properties be?).
+- 21/08/2020: Verification passes unconditionally, even in the presence of obvious bugs. This is due to the `rvfi.valid` signal from the CPU being held at constant 0. Suitable instruction and data buses as well as interrupt signals have not been wired to Minerva which is likely preventing the core and verification from functioning properly
+- 25/08/2020: Interrupts have been hardwired to zero and instruction/data buses attached to the Minerva core; however, running the verification completely hangs the machine. Possible culprit: huge number of `Assume` statements on memory values leading to overly large solution space
+
+As of 25/08
 
 ## License
 

rvfi/cores/minerva/memory_bus.py

@@ -1,4 +1,5 @@
 from nmigen import *
+from nmigen.asserts import *
 
 """
 Memory Bus (Wishbone Slave)
@@ -6,17 +7,21 @@ 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)
+        self.sel = Signal(4) # ignored during reads, just return the whole word
         self.cyc = Signal(1)
         self.stb = Signal(1)
-        self.ack = Signal(1)
+        self.ack = Signal(1, reset=0)
         self.we = Signal(1)
-        self.cti = Signal(3)
-        self.bte = Signal(2)
-        self.err = 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,
@@ -37,6 +42,67 @@ class MemoryBus(Elaboratable):
     def elaborate(self, platform):
         m = Module()
 
-        # TODO
+        # 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