From: Michael Nolan <mtnolan2640@gmail.com>
Date: Sun, 24 May 2020 15:17:12 +0000 (-0400)
Subject: Fix proof of bpermd module
X-Git-Tag: div_pipeline~877
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddb8f1d195e1ebb3c814bd154b5aaccdede82ca7;p=soc.git

Fix proof of bpermd module
---

diff --git a/src/soc/fu/logical/formal/proof_bpermd.py b/src/soc/fu/logical/formal/proof_bpermd.py
index ba93a0ef..e987f88b 100644
--- a/src/soc/fu/logical/formal/proof_bpermd.py
+++ b/src/soc/fu/logical/formal/proof_bpermd.py
@@ -95,7 +95,7 @@ class Driver(Elaboratable):
                 # 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])
+                        comb += Assert(ra[i] == rb[63-j])
 
         return m