From 0bf0e9b743aac05f25669a0891c638958f01360c Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 11:04:57 -0400 Subject: [PATCH] Formally verify OP_POPCNT --- src/soc/fu/logical/formal/proof_main_stage.py | 16 ++++++++++++---- src/soc/fu/logical/main_stage.py | 11 ++++++----- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py index 277575dc..99c88eeb 100644 --- a/src/soc/fu/logical/formal/proof_main_stage.py +++ b/src/soc/fu/logical/formal/proof_main_stage.py @@ -21,9 +21,9 @@ class Driver(Elaboratable): # inputs and outputs pass - def popcount(self, sig): + def popcount(self, sig, width): result = 0 - for i in range(sig.width): + for i in range(width): result = result + sig[i] return result @@ -79,9 +79,17 @@ class Driver(Elaboratable): comb += Assert(dut.o.o == a ^ b) with m.Case(InternalOp.OP_POPCNT): - #comb += Assume(a < ((1<<64)-1)) with m.If(rec.data_len == 8): - comb += Assert(dut.o.o == self.popcount(a)) + comb += Assert(dut.o.o == self.popcount(a, 64)) + with m.If(rec.data_len == 4): + + for i in range(2): + comb += Assert(dut.o.o[i*32:(i+1)*32] == + self.popcount(a[i*32:(i+1)*32], 32)) + with m.If(rec.data_len == 1): + for i in range(8): + comb += Assert(dut.o.o[i*8:(i+1)*8] == + self.popcount(a[i*8:(i+1)*8], 8)) return m diff --git a/src/soc/fu/logical/main_stage.py b/src/soc/fu/logical/main_stage.py index 27167ef0..9c223ddc 100644 --- a/src/soc/fu/logical/main_stage.py +++ b/src/soc/fu/logical/main_stage.py @@ -20,7 +20,8 @@ from soc.decoder.power_fieldsn import SignalBitRange def array_of(count, bitwidth): res = [] for i in range(count): - res.append(Signal(bitwidth, reset_less=True)) + res.append(Signal(bitwidth, reset_less=True, + name=f"pop_{bitwidth}_{i}")) return res @@ -82,14 +83,14 @@ class LogicalMainStage(PipeModBase): comb += dst[i].eq(Cat(src[stt], Const(0, 1)) + Cat(src[end], Const(0, 1))) # decode operation length - with m.If(op.data_len[2:4] == 0b00): + with m.If(op.data_len == 1): # popcntb - pack 8x 4-bit answers into output for i in range(8): - comb += o[i*8:i*8+4].eq(pc8[i]) - with m.Elif(op.data_len[3] == 0): + comb += o[i*8:(i+1)*8].eq(pc8[i]) + with m.Elif(op.data_len == 4): # popcntw - pack 2x 5-bit answers into output for i in range(2): - comb += o[i*32:i*32+5].eq(pc32[i]) + comb += o[i*32:(i+1)*32].eq(pc32[i]) with m.Else(): # popcntd - put 1x 6-bit answer into output comb += o.eq(popcnt[0]) -- 2.30.2