From: Michael Nolan Date: Wed, 20 May 2020 15:10:18 +0000 (-0400) Subject: Add proof for OP_PRTY X-Git-Tag: div_pipeline~1033 X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=8dd3c64cbd6b6112894f990a2cdd6661e79dd9bf Add proof for OP_PRTY --- diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py index 99c88eeb..7e69df92 100644 --- a/src/soc/fu/logical/formal/proof_main_stage.py +++ b/src/soc/fu/logical/formal/proof_main_stage.py @@ -69,6 +69,7 @@ class Driver(Elaboratable): comb += a_signed.eq(a) comb += a_signed_32.eq(a[0:32]) + comb += Assume(rec.insn_type == InternalOp.OP_PRTY) # main assertion of arithmetic operations with m.Switch(rec.insn_type): with m.Case(InternalOp.OP_AND): @@ -91,6 +92,20 @@ class Driver(Elaboratable): comb += Assert(dut.o.o[i*8:(i+1)*8] == self.popcount(a[i*8:(i+1)*8], 8)) + with m.Case(InternalOp.OP_PRTY): + with m.If(rec.data_len == 8): + result = 0 + for i in range(8): + result = result ^ a[i*8] + comb += Assert(dut.o.o == result) + with m.If(rec.data_len == 4): + result_low = 0 + result_high = 0 + for i in range(4): + result_low = result_low ^ a[i*8] + result_high = result_high ^ a[i*8 + 32] + comb += Assert(dut.o.o[0:32] == result_low) + comb += Assert(dut.o.o[32:64] == result_high) return m