Added luke's suggested code to cover all 3 assertions in proof_bperm.py

diff --git a/src/soc/fu/logical/formal/proof_bperm.py b/src/soc/fu/logical/formal/proof_bperm.py
index 453e419f51ed6fde98366a517b8d76582ab4c827..11b8e487046ca6d46dc4cbbc1f68e8dbee1502b0 100644 (file)
--- a/src/soc/fu/logical/formal/proof_bperm.py
+++ b/src/soc/fu/logical/formal/proof_bperm.py
@@ -56,7 +56,6 @@ class Driver(Elaboratable):
         comb += [rs.eq(AnyConst(64)),
                  rb.eq(AnyConst(64))]
 
-
         # The pseudocode in the Power ISA manual (v3.1) is as follows:
         # do i = 0 to 7
         #    index <- RS[8*i:8*i+8]
@@ -88,10 +87,15 @@ class Driver(Elaboratable):
         # 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]
+            index = rs[i*8:i*8+8]
             with m.If(index >= 64):
                 comb += Assert(ra[i] == 0)
-
+            with m.Else():
+                # to avoid having to create an Array of rb,
+                # cycle through from 0-63 on the index *whistle nonchalantly*
+                for j in range(64):
+                    with m.If(index == j):
+                        comb += Assert(ra[i] == rb[j])
 
         return m