From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sun, 24 May 2020 18:20:18 +0000 (+0100)
Subject: add copy of bpermd proof to logical formal proof (not nice but hey)
X-Git-Tag: div_pipeline~875
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d0d5fb047fb6d88ec24c2cca695332c76d35fc1;p=soc.git

add copy of bpermd proof to logical formal proof (not nice but hey)
---

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index cb6a0690..43dab03f 100644
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -147,8 +147,17 @@ class Driver(Elaboratable):
                 pass
 
             with m.Case(InternalOp.OP_BPERM):
-                # TODO
-                pass
+                # note that this is a copy of the beautifully-documented
+                # proof_bpermd.py
+                comb += Assert(o[8:] == 0)
+                for i in range(8):
+                    index = a[i*8:i*8+8]
+                    with m.If(index >= 64):
+                        comb += Assert(o[i] == 0)
+                    with m.Else():
+                        for j in range(64):
+                            with m.If(index == j):
+                                comb += Assert(o[i] == b[63-j])
 
             with m.Default():
                 comb += o_ok.eq(0)