Reverse order of gt combiner so it works MSB first
authorMichael Nolan <mtnolan2640@gmail.com>
Wed, 5 Feb 2020 15:06:40 +0000 (10:06 -0500)
committerMichael Nolan <mtnolan2640@gmail.com>
Wed, 5 Feb 2020 15:06:40 +0000 (10:06 -0500)
src/ieee754/part_cmp/experiments/formal/proof_gt.py
src/ieee754/part_cmp/experiments/gt_combiner.py

index 923fcf901abf215d46ee70315cd6d440dab59a4f..a1033132cec42e65d33502cc5526dbe255b0e5da 100644 (file)
@@ -50,16 +50,16 @@ class CombinerDriver(Elaboratable):
                         comb += Assert(out[i] == gts[i])
                 with m.Case(0b10):
                     comb += Assert(out[2] == gts[2])
-                    comb += Assert(out[1] == 0)
-                    comb += Assert(out[0] == (gts[0] | (eqs[0] & gts[1])))
+                    comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[0])))
+                    comb += Assert(out[0] == 0)
                 with m.Case(0b01):
-                    comb += Assert(out[2] == 0)
-                    comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[2])))
+                    comb += Assert(out[2] == (gts[2] | (eqs[2] & gts[1])))
+                    comb += Assert(out[1] == 0)
                     comb += Assert(out[0] == gts[0])
                 with m.Case(0b00):
-                    comb += Assert(out[2] == 0)
+                    comb += Assert(out[2] == (gts[2] | (eqs[2] & (gts[1] | (eqs[1] & gts[0])))))
                     comb += Assert(out[1] == 0)
-                    comb += Assert(out[0] == (gts[0] | (eqs[0] & (gts[1] | (eqs[1] & gts[2])))))
+                    comb += Assert(out[0] == 0)
         # With the aux_input set to 1, this should work similarly to
         # eq_combiner. It appears this is the case, however the
         # ungated inputs are not set to 0 like they are in eq
@@ -69,17 +69,17 @@ class CombinerDriver(Elaboratable):
                     for i in range(out.width):
                         comb += Assert(out[i] == eqs[i])
                 with m.Case(0b00):
-                    comb += Assert(out[0] == (eqs[0] & eqs[1] & eqs[2]))
+                    comb += Assert(out[2] == (eqs[0] & eqs[1] & eqs[2]))
                     comb += Assert(out[1] == 0)
-                    comb += Assert(out[2] == 0)
+                    comb += Assert(out[0] == 0)
                 with m.Case(0b10):
-                    comb += Assert(out[0] == (eqs[0] & eqs[1]))
-                    comb += Assert(out[1] == 0)
+                    comb += Assert(out[0] == 0)
+                    comb += Assert(out[1] == (eqs[0] & eqs[1]))
                     comb += Assert(out[2] == eqs[2])
                 with m.Case(0b01):
                     comb += Assert(out[0] == eqs[0])
-                    comb += Assert(out[1] == (eqs[1] & eqs[2]))
-                    comb += Assert(out[2] == 0)
+                    comb += Assert(out[1] == 0)
+                    comb += Assert(out[2] == (eqs[1] & eqs[2]))
 
 
 
@@ -100,7 +100,7 @@ class GTCombinerTestCase(FHDLTestCase):
     def test_ilang(self):
         dut = GTCombiner(3)
         vl = rtlil.convert(dut, ports=dut.ports())
-        with open("partition_combiner.il", "w") as f:
+        with open("gt_combiner.il", "w") as f:
             f.write(vl)
 
 
index 0ca8e84f1addaff2aa37a238d63f1dbf29583ac0..421a39beab1fc32a62f61fb691b775877a511c3f 100644 (file)
@@ -43,20 +43,20 @@ class GTCombiner(Elaboratable):
         m = Module()
         comb = m.d.comb
 
-        previnput = (self.gts[-1] & self.gt_en) | (self.eqs[-1] & self.aux_input)
+        previnput = (self.gts[0] & self.gt_en) | (self.eqs[0] & self.aux_input)
 
-        for i in range(self.width-1, 0, -1): # counts down from width-1 to 1
+        for i in range(self.width-1): 
             m.submodules["mux%d" % i] = mux = Combiner()
 
             comb += mux.ina.eq(previnput)
             comb += mux.inb.eq(self.aux_input)
-            comb += mux.sel.eq(self.gates[i-1])
+            comb += mux.sel.eq(self.gates[i])
             comb += self.outputs[i].eq(mux.outb)
-            previnput = (self.gts[i-1] & self.gt_en) | (self.eqs[i-1] & mux.outa)
+            previnput = (self.gts[i+1] & self.gt_en) | (self.eqs[i+1] & mux.outa)
 
-        comb += self.outputs[0].eq(previnput)
+        comb += self.outputs[-1].eq(previnput)
 
         return m
 
     def ports(self):
-        return [self.eqs, self.gts, self.gates, self.outputs]
+        return [self.eqs, self.gts, self.gates, self.outputs, self.gt_en, self.aux_input]