From 2d0d5fb047fb6d88ec24c2cca695332c76d35fc1 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton 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