From: colepoirier <colepoirier@gmail.com>
Date: Tue, 19 May 2020 00:18:59 +0000 (-0700)
Subject: Added luke's suggested code to cover all 3 assertions in proof_bperm.py
X-Git-Tag: div_pipeline~1084
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb4720571d7762a89c9b9f1681c99c0fe5f7d496;p=soc.git

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 453e419f..11b8e487 100644
--- 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