[libre-riscv-dev] [Bug 316] bperm TODO

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 19 00:54:31 BST 2020


https://bugs.libre-soc.org/show_bug.cgi?id=316

--- Comment #45 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
err *cough* really-bad-hack mumble *cough*

index 453e419..0f879e3 100644
--- a/src/soc/fu/logical/formal/proof_bperm.py
+++ b/src/soc/fu/logical/formal/proof_bperm.py
@@ -88,9 +88,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

-- 
You are receiving this mail because:
You are on the CC list for the bug.


More information about the libre-riscv-dev mailing list