From 2d0d5fb047fb6d88ec24c2cca695332c76d35fc1 Mon Sep 17 00:00:00 2001
From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sun, 24 May 2020 19:20:18 +0100
Subject: [PATCH] add copy of bpermd proof to logical formal proof (not nice
but hey)
---
src/soc/fu/logical/formal/proof_main_stage.py | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
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)
--
2.30.2