From 84f7cf502d8d80a8198530aa0ef4611140dd500d Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 27 May 2020 16:40:18 +0100 Subject: [PATCH] cleanup logical main proof --- src/soc/fu/logical/formal/proof_main_stage.py | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) 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): -- 2.30.2