From a1f49befd9b61093c4b8017fe7ba1242022b4c90 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Thu, 14 May 2020 10:35:44 -0400 Subject: [PATCH] Fix bug in shift_rot, update proof to handle new interface --- src/soc/shift_rot/formal/proof_main_stage.py | 7 +++++-- src/soc/shift_rot/rotator.py | 2 +- src/soc/shift_rot/test/test_pipe_caller.py | 9 +++++---- 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/soc/shift_rot/formal/proof_main_stage.py b/src/soc/shift_rot/formal/proof_main_stage.py index 2cb2b0d1..50264d5c 100644 --- a/src/soc/shift_rot/formal/proof_main_stage.py +++ b/src/soc/shift_rot/formal/proof_main_stage.py @@ -37,8 +37,9 @@ class Driver(Elaboratable): m.submodules.dut = dut = ShiftRotMainStage(pspec) # convenience variables - a = dut.i.a - b = dut.i.b + a = dut.i.rs + b = dut.i.rb + ra = dut.i.ra carry_in = dut.i.carry_in so_in = dut.i.so carry_out = dut.o.carry_out @@ -67,12 +68,14 @@ class Driver(Elaboratable): # main assertion of arithmetic operations with m.Switch(rec.insn_type): with m.Case(InternalOp.OP_SHL): + 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(): comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1))) with m.Case(InternalOp.OP_SHR): + comb += Assume(ra == 0) with m.If(~rec.is_signed): with m.If(rec.is_32bit): comb += Assert(o[0:32] == (a[0:32] >> b[0:6])) diff --git a/src/soc/shift_rot/rotator.py b/src/soc/shift_rot/rotator.py index b695a4e1..60694729 100644 --- a/src/soc/shift_rot/rotator.py +++ b/src/soc/shift_rot/rotator.py @@ -122,7 +122,7 @@ class Rotator(Elaboratable): comb += me.eq(Cat(self.mb, self.mb_extra, Const(0b0, 1))) with m.Else(): # effectively, 63 - sh - comb += me.eq(Cat(~self.shift[0:6], self.shift[6])) + comb += me.eq(Cat(~sh[0:6], sh[6])) # Calculate left and right masks comb += mr.eq(right_mask(m, mb)) diff --git a/src/soc/shift_rot/test/test_pipe_caller.py b/src/soc/shift_rot/test/test_pipe_caller.py index e1ca7fc5..97df2f20 100644 --- a/src/soc/shift_rot/test/test_pipe_caller.py +++ b/src/soc/shift_rot/test/test_pipe_caller.py @@ -123,11 +123,12 @@ class ALUTestCase(FHDLTestCase): self.run_tst_program(Program(lst), initial_regs) def test_shift_once(self): - lst = ["sraw 3, 1, 2"] + lst = ["slw 3, 1, 4", + "slw 3, 1, 2"] initial_regs = [0] * 32 - initial_regs[1] = 0xdeadbeefcafec0de - initial_regs[2] = 53 - print(initial_regs[1], initial_regs[2]) + initial_regs[1] = 0x80000000 + initial_regs[2] = 0x40 + initial_regs[4] = 0x00 self.run_tst_program(Program(lst), initial_regs) def test_rlwinm(self): -- 2.30.2