From a66c0b3af29e20ac26d81d41d2b7e8233d4db070 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Mon, 13 Jul 2020 16:07:09 +0100 Subject: [PATCH] attempting formal proof of OP_EXTSWSLI --- .../fu/shift_rot/formal/proof_main_stage.py | 23 ++++++++++++++----- src/soc/fu/shift_rot/test/test_pipe_caller.py | 14 ++++++++++- 2 files changed, 30 insertions(+), 7 deletions(-) diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py index 6346950d..e6e8b7c7 100644 --- a/src/soc/fu/shift_rot/formal/proof_main_stage.py +++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py @@ -16,6 +16,7 @@ from soc.fu.alu.pipe_data import ALUPipeSpec from soc.fu.alu.alu_input_record import CompALUOpSubset from soc.decoder.power_enums import MicrOp import unittest +from nmutil.extend import exts # This defines a module to drive the device under test and assert @@ -47,11 +48,10 @@ class Driver(Elaboratable): o = dut.o.o.data # setup random inputs - comb += [a.eq(AnyConst(64)), - b.eq(AnyConst(64)), - carry_in.eq(AnyConst(1)), - carry_in32.eq(AnyConst(1)), - ] + comb += a.eq(AnyConst(64)) + comb += b.eq(AnyConst(64)) + comb += carry_in.eq(AnyConst(1)) + comb += carry_in32.eq(AnyConst(1)) comb += dut.i.ctx.op.eq(rec) @@ -104,7 +104,18 @@ class Driver(Elaboratable): with m.Case(MicrOp.OP_RLCL): pass with m.Case(MicrOp.OP_EXTSWSLI): - pass + # sign-extend + a_s = Signal(64, reset_less=True) + comb += a_s.eq(exts(a, 32, 64)) + # assume b[0:6] is sh + comb += Assume(b[7:] == 0) + with m.If(b[0:7] == 0): + comb += Assert(o[0:32] == a_s[0:32]) + with m.Else(): + #b_s = 64-b[0:6] + #comb += Assert(o == ((a_s << b_s) & ((1 << 64)-1))) + pass + with m.Default(): comb += o_ok.eq(0) diff --git a/src/soc/fu/shift_rot/test/test_pipe_caller.py b/src/soc/fu/shift_rot/test/test_pipe_caller.py index ec35aaae..ee11bad2 100644 --- a/src/soc/fu/shift_rot/test/test_pipe_caller.py +++ b/src/soc/fu/shift_rot/test/test_pipe_caller.py @@ -142,12 +142,24 @@ class ShiftRotTestCase(FHDLTestCase): self.run_tst_program(Program(lst, bigendian), initial_regs) def test_regression_extswsli(self): - sh = random.randint(0, 63) lst = [f"extswsli 3, 1, 34"] initial_regs = [0] * 32 initial_regs[1] = 0x5678 self.run_tst_program(Program(lst, bigendian), initial_regs) + def test_regression_extswsli_2(self): + lst = [f"extswsli 3, 1, 7"] + initial_regs = [0] * 32 + initial_regs[1] = 0x3ffffd7377f19fdd + self.run_tst_program(Program(lst, bigendian), initial_regs) + + def test_regression_extswsli_3(self): + lst = [f"extswsli 3, 1, 0"] + initial_regs = [0] * 32 + initial_regs[1] = 0x80000000fb4013e2 + #initial_regs[1] = 0x3ffffd73f7f19fdd + self.run_tst_program(Program(lst, bigendian), initial_regs) + def test_extswsli(self): for i in range(40): sh = random.randint(0, 63) -- 2.30.2