From 16ac8bcd32bd2998d58488ca236f8ff721eccaf6 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 14:51:17 -0400 Subject: [PATCH] Add proof for OP_CROP --- src/soc/fu/cr/formal/proof_main_stage.py | 42 ++++++++++++++++++++++-- 1 file changed, 39 insertions(+), 3 deletions(-) diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py index caf45290..18d0d1d8 100644 --- a/src/soc/fu/cr/formal/proof_main_stage.py +++ b/src/soc/fu/cr/formal/proof_main_stage.py @@ -52,16 +52,52 @@ class Driver(Elaboratable): dut_sig = getattr(dut.o.ctx.op, name) comb += Assert(dut_sig == rec_sig) - cr_arr = Array([cr[i] for i in range(32)]) - cr_o_arr = Array([cr[i] for i in range(32)]) + # big endian indexing. *sigh* + cr_arr = Array([cr[31-i] for i in range(32)]) + cr_o_arr = Array([cr_o[31-i] for i in range(32)]) + xl_fields = dut.fields.FormXL + xfx_fields = dut.fields.FormXFX with m.Switch(rec.insn_type): with m.Case(InternalOp.OP_MTCRF): - xfx_fields = dut.fields.FormXFX FXM = xfx_fields.FXM[0:-1] for i in range(8): with m.If(FXM[i]): comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4]) + with m.Case(InternalOp.OP_CROP): + bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True) + ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True) + bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True) + comb += bt.eq(xl_fields.BT[0:-1]) + comb += ba.eq(xl_fields.BA[0:-1]) + comb += bb.eq(xl_fields.BB[0:-1]) + + bit_a = Signal() + bit_b = Signal() + bit_o = Signal() + comb += bit_a.eq(cr_arr[ba]) + comb += bit_b.eq(cr_arr[bb]) + comb += bit_o.eq(cr_o_arr[bt]) + + lut = Signal(4) + comb += lut.eq(rec.insn[6:10]) + with m.If(lut == 0b1000): + comb += Assert(bit_o == bit_a & bit_b) + with m.If(lut == 0b0100): + comb += Assert(bit_o == bit_a & ~bit_b) + with m.If(lut == 0b1001): + comb += Assert(bit_o == ~(bit_a ^ bit_b)) + with m.If(lut == 0b0111): + comb += Assert(bit_o == ~(bit_a & bit_b)) + with m.If(lut == 0b0001): + comb += Assert(bit_o == ~(bit_a | bit_b)) + with m.If(lut == 0b1110): + comb += Assert(bit_o == bit_a | bit_b) + with m.If(lut == 0b1101): + comb += Assert(bit_o == bit_a | ~bit_b) + with m.If(lut == 0b0110): + comb += Assert(bit_o == bit_a ^ bit_b) + return m -- 2.30.2