From 647aeb78f14644cea48d111b713bbef0073a5a12 Mon Sep 17 00:00:00 2001
From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 26 May 2020 12:43:57 +0100
Subject: [PATCH] whitespace, add commentary

---
 src/soc/fu/compunits/formal/proof_fu.py | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py
index f4bb8aa7..c2b964c5 100644
--- a/src/soc/fu/compunits/formal/proof_fu.py
+++ b/src/soc/fu/compunits/formal/proof_fu.py
@@ -4,7 +4,6 @@
 
 # This attempts to prove most of the bullet points on that page
 
-
 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
                     signed, ResetSignal)
 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
@@ -18,6 +17,7 @@ from soc.experiment.alu_hier import DummyALU
 from soc.experiment.compalu_multi import MultiCompUnit
 from soc.fu.alu.alu_input_record import CompALUOpSubset
 
+
 class Driver(Elaboratable):
     def __init__(self):
         pass
@@ -27,8 +27,7 @@ class Driver(Elaboratable):
         comb = m.d.comb
         sync = m.d.sync
         alu = DummyALU(16)
-        m.submodules.dut = dut = MultiCompUnit(16, alu,
-                                               CompALUOpSubset)
+        m.submodules.dut = dut = MultiCompUnit(16, alu, CompALUOpSubset)
 
         issue = dut.issue_i
         busy = dut.busy_o
@@ -49,8 +48,6 @@ class Driver(Elaboratable):
 
         has_issued = Signal(reset=0)
 
-
-
         with m.If(init):
             comb += Assume(has_issued == 0)
             comb += Assume(issue == 0)
@@ -121,14 +118,12 @@ class Driver(Elaboratable):
             with m.If(wr_rel == 0):
                 comb += Assume(go_wr == 0)
 
-
             # Property 9: Similar to property 5, 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 10: Similar to property 6, wr_rel should be
             # deasserted when go_die is asserted
             with m.If(Past(wr_rel) & Past(go_die)):
@@ -141,12 +136,19 @@ class Driver(Elaboratable):
 
             # Assume no instruction is issued until rd_rel is
             # released. Idk if this is valid
+            # (lkcl notes: it's actually that no instruction is issued
+            # until *busy* is released.  oh i think i see what you
+            # mean: well... kinda.  because rd_rel relies on wr_rel
+            # and wr_rel relies on instruction, there exists a
+            # transitive relationship, which is not strictly necessary to
+            # explicitly check)
 
             with m.If(busy):
                 comb += Assume(issue == 0)
 
         return m
 
+
 class FUTestCase(FHDLTestCase):
     def test_formal(self):
         module = Driver()
-- 
2.30.2