From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 27 May 2020 15:40:18 +0000 (+0100)
Subject: cleanup logical main proof
X-Git-Tag: div_pipeline~789
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=84f7cf502d8d80a8198530aa0ef4611140dd500d;p=soc.git

cleanup logical main proof
---

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 9e6d17a2..d37bec3d 100644
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -89,14 +89,13 @@ class Driver(Elaboratable):
                 with m.If(rec.data_len == 8):
                     comb += Assert(o == self.popcount(a, 64))
                 with m.If(rec.data_len == 4):
-
                     for i in range(2):
-                        comb += Assert(o[i*32:(i+1)*32] ==
-                                       self.popcount(a[i*32:(i+1)*32], 32))
+                        slc = slice(i*32, (i+1)*32)
+                        comb += Assert(o[slc] == self.popcount(a[slc], 32))
                 with m.If(rec.data_len == 1):
                     for i in range(8):
-                        comb += Assert(o[i*8:(i+1)*8] ==
-                                       self.popcount(a[i*8:(i+1)*8], 8))
+                        slc = slice(i*8, (i+1)*8)
+                        comb += Assert(o[slc] == self.popcount(a[slc], 8))
 
             with m.Case(InternalOp.OP_PRTY):
                 with m.If(rec.data_len == 8):