Add shift left and shift right to main stage proof

diff --git a/src/soc/alu/formal/proof_main_stage.py b/src/soc/alu/formal/proof_main_stage.py
index ea74dd18883d7c3bcf0956e7316adc4f452459ed..19100079c9ae5ccacf4352bc1b7bd453e5b55a9e 100644 (file)
--- a/src/soc/alu/formal/proof_main_stage.py
+++ b/src/soc/alu/formal/proof_main_stage.py
@@ -1,7 +1,8 @@
 # Proof of correctness for partitioned equal signal combiner
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
-from nmigen import Module, Signal, Elaboratable, Mux, Cat
+from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
+                    signed)
 from nmigen.asserts import Assert, AnyConst, Assume, Cover
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil
@@ -59,6 +60,11 @@ class Driver(Elaboratable):
             dut_sig = getattr(dut.o.ctx.op, name)
             comb += Assert(dut_sig == rec_sig)
 
+        a_signed = Signal(signed(64))
+        comb += a_signed.eq(a)
+        a_signed_32 = Signal(signed(32))
+        comb += a_signed_32.eq(a[0:32])
+
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_ADD):
                 comb += Assert(Cat(dut.o.o, dut.o.carry_out) ==
@@ -69,6 +75,29 @@ class Driver(Elaboratable):
                 comb += Assert(dut.o.o == a | b)
             with m.Case(InternalOp.OP_XOR):
                 comb += Assert(dut.o.o == a ^ b)
+            with m.Case(InternalOp.OP_SHL):
+                with m.If(rec.is_32bit):
+                    comb += Assert(dut.o.o[0:32] == ((a << b[0:6]) &
+                                                     0xffffffff))
+                    comb += Assert(dut.o.o[32:64] == 0)
+                with m.Else():
+                    comb += Assert(dut.o.o == ((a << b[0:7]) &
+                                               ((1 << 64)-1)))
+            with m.Case(InternalOp.OP_SHR):
+                with m.If(~rec.is_signed):
+                    with m.If(rec.is_32bit):
+                        comb += Assert(dut.o.o[0:32] ==
+                                       (a[0:32] >> b[0:6]))
+                        comb += Assert(dut.o.o[32:64] == 0)
+                    with m.Else():
+                        comb += Assert(dut.o.o == (a >> b[0:7]))
+                with m.Else():
+                    with m.If(rec.is_32bit):
+                        comb += Assert(dut.o.o[0:32] ==
+                                       (a_signed_32 >> b[0:6]))
+                        comb += Assert(dut.o.o[32:64] == Repl(a[31], 32))
+                    with m.Else():
+                        comb += Assert(dut.o.o == (a_signed >> b[0:7]))
 
 
         return m

diff --git a/src/soc/alu/test/test_pipe_caller.py b/src/soc/alu/test/test_pipe_caller.py
index 581fef1b8caca470655b8d079afc651b36c56ec2..9fff62c9d6ab74df2fdeb8b971d86e5d36ee9251 100644 (file)
--- a/src/soc/alu/test/test_pipe_caller.py
+++ b/src/soc/alu/test/test_pipe_caller.py
@@ -145,7 +145,6 @@ class ALUTestCase(FHDLTestCase):
         with Program(lst) as program:
             sim = self.run_tst_program(program, initial_regs)
 
-    @unittest.skip("broken")
     def test_ilang(self):
         rec = CompALUOpSubset()