From: Michael Nolan <mtnolan2640@gmail.com>
Date: Fri, 8 May 2020 15:09:40 +0000 (-0400)
Subject: Add handling of A inversion and B input
X-Git-Tag: div_pipeline~1346
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bac3a07250026743e1521154d9dc82ddacbcb825;p=soc.git

Add handling of A inversion and B input
---

diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py
index faf68e07..22cd52bf 100644
--- a/src/soc/alu/formal/proof_input_stage.py
+++ b/src/soc/alu/formal/proof_input_stage.py
@@ -26,20 +26,37 @@ class Driver(Elaboratable):
         pspec = ALUPipeSpec()
         m.submodules.dut = dut = ALUInputStage(pspec)
 
+        a = Signal(64)
+        b = Signal(64)
+        comb += [dut.i.a.eq(a),
+                 dut.i.b.eq(b),
+                 a.eq(AnyConst(64)),
+                 b.eq(AnyConst(64))]
+                      
+        # Setup random inputs for dut.op
         rec = CompALUOpSubset()
-
         for p in rec.ports():
             width = p.width
             comb += p.eq(AnyConst(width))
 
         comb += dut.i.op.eq(rec)
 
+
+        # Assert that op gets copied from the input to output
         for p in rec.ports():
             name = p.name
             rec_sig = p
             dut_sig = getattr(dut.o.op, name)
             comb += Assert(dut_sig == rec_sig)
 
+        with m.If(rec.invert_a):
+            comb += Assert(dut.o.a == ~a)
+        with m.Else():
+            comb += Assert(dut.o.a == a)
+        comb += Assert(dut.o.b == b)
+
+
+
 
         return m
 
diff --git a/src/soc/alu/input_stage.py b/src/soc/alu/input_stage.py
index 5bcff4f2..ccf00301 100644
--- a/src/soc/alu/input_stage.py
+++ b/src/soc/alu/input_stage.py
@@ -20,4 +20,15 @@ class ALUInputStage(PipeModBase):
 
         comb += self.o.op.eq(self.i.op)
 
+        a = Signal.like(self.i.a)
+
+        with m.If(self.i.op.invert_a):
+            comb += a.eq(~self.i.a)
+        with m.Else():
+            comb += a.eq(self.i.a)
+
+        comb += self.o.a.eq(a)
+
+        comb += self.o.b.eq(self.i.b)
+
         return m