From 21f5fbd55b42fd211604b9902eeb06996a1b7fb5 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Mon, 13 Jul 2020 20:28:11 +0100 Subject: [PATCH] formal proof of OP_EXTSWSLI --- .../fu/shift_rot/formal/proof_main_stage.py | 28 ++++++++++--------- src/soc/fu/shift_rot/test/test_pipe_caller.py | 5 +++- 2 files changed, 19 insertions(+), 14 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 21ce002f..582c6745 100644 --- a/src/soc/fu/shift_rot/formal/proof_main_stage.py +++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py @@ -75,6 +75,7 @@ class Driver(Elaboratable): # main assertion of arithmetic operations with m.Switch(rec.insn_type): + # left-shift: 64/32-bit with m.Case(MicrOp.OP_SHL): comb += Assume(ra == 0) with m.If(rec.is_32bit): @@ -83,6 +84,7 @@ class Driver(Elaboratable): with m.Else(): comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1))) + # right-shift: 64/32-bit / signed with m.Case(MicrOp.OP_SHR): comb += Assume(ra == 0) with m.If(~rec.is_signed): @@ -97,6 +99,19 @@ class Driver(Elaboratable): comb += Assert(o[32:64] == Repl(a[31], 32)) with m.Else(): comb += Assert(o == (a_signed >> b[0:7])) + + # extswsli: 32/64-bit moded + with m.Case(MicrOp.OP_EXTSWSLI): + comb += Assume(ra == 0) + with m.If(rec.is_32bit): + comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff)) + comb += Assert(o[32:64] == 0) + with m.Else(): + # sign-extend to 64 bit + a_s = Signal(64, reset_less=True) + comb += a_s.eq(exts(a, 32, 64)) + comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1))) + #TODO with m.Case(MicrOp.OP_RLC): pass @@ -104,19 +119,6 @@ class Driver(Elaboratable): pass with m.Case(MicrOp.OP_RLCL): pass - with m.Case(MicrOp.OP_EXTSWSLI): - # 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 ee11bad2..6e48cb2c 100644 --- a/src/soc/fu/shift_rot/test/test_pipe_caller.py +++ b/src/soc/fu/shift_rot/test/test_pipe_caller.py @@ -156,7 +156,10 @@ class ShiftRotTestCase(FHDLTestCase): def test_regression_extswsli_3(self): lst = [f"extswsli 3, 1, 0"] initial_regs = [0] * 32 - initial_regs[1] = 0x80000000fb4013e2 + #initial_regs[1] = 0x80000000fb4013e2 + #initial_regs[1] = 0xffffffffffffffff + #initial_regs[1] = 0x00000000ffffffff + initial_regs[1] = 0x0000010180122900 #initial_regs[1] = 0x3ffffd73f7f19fdd self.run_tst_program(Program(lst, bigendian), initial_regs) -- 2.30.2