From f9b86cecd00d7554e92ced708800b95b173a59e0 Mon Sep 17 00:00:00 2001
From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 25 May 2020 14:28:42 -0400
Subject: [PATCH] Add assertions about go_wr and wr_rel

---
 src/soc/fu/compunits/formal/proof_fu.py | 49 ++++++++++++++++++++++---
 1 file changed, 44 insertions(+), 5 deletions(-)

diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py
index 0644587b..86246592 100644
--- a/src/soc/fu/compunits/formal/proof_fu.py
+++ b/src/soc/fu/compunits/formal/proof_fu.py
@@ -23,11 +23,16 @@ class Driver(Elaboratable):
         m.submodules.dut = dut = MultiCompUnit(16, alu,
                                                CompALUOpSubset)
 
+        issue = dut.issue_i
+
         go_rd = dut.rd.go
         rd_rel = dut.rd.rel
-        issue = dut.issue_i
+
+        go_wr = dut.wr.go
+        wr_rel = dut.wr.rel
 
         go_die = dut.go_die_i
+        shadow = dut.shadown_i
 
         rst = ResetSignal()
 
@@ -50,26 +55,26 @@ class Driver(Elaboratable):
                 sync += has_issued.eq(1)
                 comb += Cover(has_issued)
 
-            # Property One: Rd_rel should never be asserted before issue
+            # Property 1: Rd_rel should never be asserted before issue
 
             # If issue has never been raised, then rd_rel should never
             # be raised
             with m.If(rd_rel != 0):
                 comb += Assert(has_issued)
 
-            # Property Two: when rd_rel is asserted, it should stay
+            # Property 2: when rd_rel is asserted, it should stay
             # that way until a go_rd
             with m.If((Past(go_rd) == 0) & ~Past(go_die)):
                 comb += Assert(~Fell(rd_rel))
 
-            # Property Three: when a bit in rd_rel is asserted, and
+            # Property 3: when a bit in rd_rel is asserted, and
             # the corresponding bit in go_rd is asserted, then that
             # bit of rd_rel should be deasserted
             for i in range(2):
                 with m.If(Past(go_rd)[i] & (Past(rd_rel) != 0)):
                     comb += Assert(rd_rel[i] == ~Past(go_rd)[i])
 
-            # Property Four: Similarly, if rd_rel is asserted,
+            # Property 4: Similarly, if rd_rel is asserted,
             # asserting go_die should make rd_rel be deasserted
 
             with m.If(Past(rd_rel) != 0):
@@ -78,6 +83,40 @@ class Driver(Elaboratable):
 
             comb += Cover(Fell(rd_rel))
 
+            # Property 5: Similar to property 1, wr_rel should
+            # never be asserted unless there was a preceeding issue
+
+            with m.If(wr_rel != 0):
+                comb += Assert(has_issued)
+
+            # Property 6: Similar to property 2, wr_rel should stay
+            # asserted until a go_rd, go_die, or shadow
+
+            with m.If((Past(go_wr) == 0) & ~Past(go_die, 2) &
+                      ~Past(shadow)):
+                comb += Assert(~Fell(wr_rel))
+            # Assume go_wr is not asserted unless wr_rel is
+            with m.If(wr_rel == 0):
+                comb += Assume(go_wr == 0)
+
+
+            # Property 7: Similar to property 3, when wr_rel is
+            # asserted and go_wr is asserted, then wr_rel should be
+            # deasserted
+            with m.If(Past(wr_rel) & Past(go_wr)):
+                comb += Assert(wr_rel == 0)
+
+
+            # Property 8: Similar to property 4, wr_rel should be
+            # deasserted when go_die is asserted
+            with m.If(Past(wr_rel) & Past(go_die)):
+                comb += Assert(wr_rel == 0)
+
+            # Property 9: wr_rel should not fall while shadow is
+            # asserted
+            with m.If(wr_rel & shadow):
+                comb += Assert(~Fell(wr_rel))
+
             # Assume no instruction is issued until rd_rel is
             # released. Idk if this is valid
 
-- 
2.30.2