From 5d21832c5704a1db619b290b8b669f0e5efb68cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= <jf@jfng.fr>
Date: Wed, 13 Jul 2022 20:36:12 +0200
Subject: [PATCH] pfv.Interface: simplify memory port.

The former `pfv.insn_mem` field was redundant with `pfv.insn` and
`pfv.cia`.

Also, validate memory port properties in InsnTestbench.
---
 power_fv/check/insn/__init__.py | 45 +++++++++++++++++++++++++++++++++
 power_fv/pfv.py                 | 41 ++++++++++--------------------
 2 files changed, 59 insertions(+), 27 deletions(-)

diff --git a/power_fv/check/insn/__init__.py b/power_fv/check/insn/__init__.py
index 3ff867a..13cc934 100644
--- a/power_fv/check/insn/__init__.py
+++ b/power_fv/check/insn/__init__.py
@@ -1,6 +1,7 @@
 from amaranth import *
 from amaranth.asserts import *
 
+from power_fv.pfv import mem_port_layout
 from power_fv.check import PowerFVCheck, PowerFVCheckMeta
 from power_fv.check._timer import Timer
 
@@ -85,6 +86,13 @@ class InsnTestbench(Elaboratable):
                 Assert(rt.valid.all()),
             ]
 
+        m.submodules.mem = mem = _MemPortTest(self.check)
+
+        m.d.comb += spec.pfv.mem.r_data.eq(dut.pfv.mem.r_data)
+
+        with m.If(t_post.zero & ~spec.pfv.intr):
+            m.d.comb += Assert(mem.valid.all())
+
         m.submodules.cr   = cr   = _SysRegTest(self.check, reg="cr"  )
         m.submodules.msr  = msr  = _SysRegTest(self.check, reg="msr" )
         m.submodules.lr   = lr   = _SysRegTest(self.check, reg="lr"  )
@@ -155,6 +163,43 @@ class _GPRFileTest(Elaboratable):
         return m
 
 
+class _MemPortTest(Elaboratable):
+    def __init__(self, check):
+        self._dut  = check.dut .pfv.mem
+        self._spec = check.spec.pfv.mem
+
+        self.valid = Record([
+            ("read",  [("addr", 1), ("r_mask", 1)]),
+            ("write", [("addr", 1), ("w_mask", 1), ("w_data", 1)]),
+        ])
+
+    def elaborate(self, platform):
+        m = Module()
+
+        dut  = Record(mem_port_layout())
+        spec = Record(mem_port_layout())
+
+        def contains(a, mask, b):
+            mask_8 = Cat(Repl(bit, 8) for bit in mask)
+            return a & mask_8 == b & mask_8
+
+        m.d.comb += [
+            dut .eq(self._dut),
+            spec.eq(self._spec),
+
+            # The DUT and the spec must read from the same bits at the same address.
+            self.valid.read.addr  .eq(spec.r_mask.any().implies(dut.addr == spec.addr)),
+            self.valid.read.r_mask.eq(spec.r_mask == dut.r_mask),
+
+            # The DUT and the spec must write the same value to the same bits at the same address.
+            self.valid.write.addr  .eq(spec.w_mask.any().implies(dut.addr == spec.addr)),
+            self.valid.write.w_mask.eq(spec.w_mask == dut.w_mask),
+            self.valid.write.w_data.eq(contains(dut.w_data, spec.w_mask, spec.w_data)),
+        ]
+
+        return m
+
+
 class _SysRegTest(Elaboratable):
     def __init__(self, check, *, reg):
         self._dut  = getattr(check.dut .pfv, reg)
diff --git a/power_fv/pfv.py b/power_fv/pfv.py
index 23e1b6d..d5adbff 100644
--- a/power_fv/pfv.py
+++ b/power_fv/pfv.py
@@ -5,7 +5,7 @@ from power_fv.reg import *
 
 
 __all__ = [
-    "gprf_port_layout", "reg_port_layout", "mem_port_layout",
+    "gprf_port_layout", "mem_port_layout", "reg_port_layout",
     "Interface",
 ]
 
@@ -20,6 +20,17 @@ def gprf_port_layout():
     ]
 
 
+def mem_port_layout():
+    layout = [
+        ("addr",   unsigned(64)),
+        ("r_mask", unsigned( 8)),
+        ("r_data", unsigned(64)),
+        ("w_mask", unsigned( 8)),
+        ("w_data", unsigned(64)),
+    ]
+    return layout
+
+
 def reg_port_layout(reg_layout):
     return [
         ("r_mask",  reg_layout),
@@ -29,29 +40,6 @@ def reg_port_layout(reg_layout):
     ]
 
 
-def mem_port_layout(access):
-    if access not in ("r", "rw"):
-        raise ValueError("Access mode must be \"r\" or \"rw\", not {!r}"
-                        .format(access))
-
-    granularity = 8
-    data_width  = 64
-    mask_width  = data_width // granularity
-    addr_width  = 64 - log2_int(data_width // granularity)
-
-    access_layout = [
-        ("mask", unsigned(mask_width)),
-        ("data", unsigned(data_width)),
-    ]
-
-    layout = [("addr", unsigned(addr_width))]
-    if "r" in access:
-        layout += [("r", access_layout)]
-    if "w" in access:
-        layout += [("w", access_layout)]
-    return layout
-
-
 class Interface(Record):
     """Power-FV interface.
 
@@ -77,6 +65,8 @@ class Interface(Record):
             ("rs", gprf_port_layout()),
             ("rt", gprf_port_layout()),
 
+            ("mem", mem_port_layout()),
+
             ("cr"  , reg_port_layout(  cr_layout)),
             ("msr" , reg_port_layout( msr_layout)),
             ("lr"  , reg_port_layout(  lr_layout)),
@@ -85,8 +75,5 @@ class Interface(Record):
             ("xer" , reg_port_layout( xer_layout)),
             ("srr0", reg_port_layout(srr0_layout)),
             ("srr1", reg_port_layout(srr1_layout)),
-
-            ("insn_mem", mem_port_layout(access="r" )),
-            ("data_mem", mem_port_layout(access="rw")),
         ]
         super().__init__(layout, name=name, src_loc_at=1 + src_loc_at)