Added 2nd of 3 assertions for proof_bperm.py, currently not correct

diff --git a/src/soc/fu/logical/formal/proof_bperm.py b/src/soc/fu/logical/formal/proof_bperm.py
index 02d63cb8a4ec672b4b2878c5d7c18cd2cdbd8137..453e419f51ed6fde98366a517b8d76582ab4c827 100644 (file)
--- a/src/soc/fu/logical/formal/proof_bperm.py
+++ b/src/soc/fu/logical/formal/proof_bperm.py
@@ -87,7 +87,10 @@ class Driver(Elaboratable):
         # checking if the index is >= 64 (it's hardware, so use an
         # m.If()). Finally, I'd add an assert that checks whether
         # ra[i] is equal to 0
-
+        for i in range(8):
+            index = rb[i*8:i*8+8]
+            with m.If(index >= 64):
+                comb += Assert(ra[i] == 0)
 
 
         return m
@@ -108,7 +111,7 @@ class TestCase(FHDLTestCase):
         # and steps it through `depth` cycles, checking that the
         # assertions hold at every cycle. Since this is a
         # combinatorial module, it only needs 1 cycle to prove
-        # everything. 
+        # everything.
         self.assertFormal(module, mode="bmc", depth=2)
         self.assertFormal(module, mode="cover", depth=2)