From fc9feb58cb6812f37d401ff4c1d35678724cb261 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= <jf@jfng.fr>
Date: Fri, 15 Apr 2022 16:05:11 +0200
Subject: [PATCH] checks.unique: add check.

---
 power_fv/checks/__init__.py |  1 +
 power_fv/checks/unique.py   | 66 +++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 power_fv/checks/unique.py

diff --git a/power_fv/checks/__init__.py b/power_fv/checks/__init__.py
index e69de29..a2dccb0 100644
--- a/power_fv/checks/__init__.py
+++ b/power_fv/checks/__init__.py
@@ -0,0 +1 @@
+from .unique import *
diff --git a/power_fv/checks/unique.py b/power_fv/checks/unique.py
new file mode 100644
index 0000000..483a86b
--- /dev/null
+++ b/power_fv/checks/unique.py
@@ -0,0 +1,66 @@
+from amaranth import *
+from amaranth.asserts import *
+
+from .. import pfv
+
+
+__all__ = ["UniquenessCheck", "UniquenessCover"]
+
+
+class UniquenessCheck(Elaboratable):
+    """Uniqueness check.
+
+    Check that the core cannot retire two instructions with the same `pfv.order` identifier.
+    """
+    def __init__(self):
+        self.pre  = Signal()
+        self.post = Signal()
+        self.pfv  = pfv.Interface()
+
+    def elaborate(self, platform):
+        m = Module()
+
+        spec_order = AnyConst(self.pfv.order.shape())
+        duplicate  = Signal()
+
+        with m.If(self.pre):
+            m.d.sync += [
+                Assume(self.pfv.stb),
+                Assume(spec_order == self.pfv.order),
+                Assume(~duplicate),
+            ]
+        with m.Elif(self.pfv.stb & (self.pfv.order == spec_order)):
+            m.d.sync += duplicate.eq(1)
+
+        with m.If(self.post):
+            m.d.sync += Assert(~duplicate)
+
+        return m
+
+
+class UniquenessCover(Elaboratable):
+    def __init__(self):
+        self.pre  = Signal()
+        self.post = Signal()
+        self.pfv  = pfv.Interface()
+
+    def elaborate(self, platform):
+        m = Module()
+
+        insn_count = Signal(range(4))
+
+        with m.If(self.pfv.stb):
+            m.d.sync += insn_count.eq(insn_count + 1)
+
+        cover_1 = Signal()
+        cover_2 = Signal()
+
+        m.d.comb += [
+            cover_1.eq(insn_count == 1),
+            cover_2.eq(insn_count == 2),
+
+            Cover(cover_1),
+            Cover(cover_2),
+        ]
+
+        return m