Convert alu to use the op in ctx
authorMichael Nolan <mtnolan2640@gmail.com>
Fri, 8 May 2020 16:35:51 +0000 (12:35 -0400)
committerMichael Nolan <mtnolan2640@gmail.com>
Fri, 8 May 2020 16:35:51 +0000 (12:35 -0400)
src/soc/alu/formal/proof_input_stage.py
src/soc/alu/input_stage.py
src/soc/alu/pipe_data.py

index b11ec4f303541d816fa663a20e5569cf35a110e4..ab679e01e25352a872398103cbe2639448a25dad 100644 (file)
@@ -23,7 +23,15 @@ class Driver(Elaboratable):
         m = Module()
         comb = m.d.comb
 
-        pspec = ALUPipeSpec(id_wid=2, op_wid=1)
+        rec = CompALUOpSubset()
+        recwidth = 0
+        # Setup random inputs for dut.op
+        for p in rec.ports():
+            width = p.width
+            recwidth += width
+            comb += p.eq(AnyConst(width))
+
+        pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
         m.submodules.dut = dut = ALUInputStage(pspec)
 
         a = Signal(64)
@@ -33,20 +41,15 @@ class Driver(Elaboratable):
                  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)
+        comb += dut.i.ctx.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)
+            dut_sig = getattr(dut.o.ctx.op, name)
             comb += Assert(dut_sig == rec_sig)
 
         with m.If(rec.invert_a):
@@ -61,7 +64,7 @@ class Driver(Elaboratable):
         return m
 
 class GTCombinerTestCase(FHDLTestCase):
-    def test_gt_combiner(self):
+    def test_formal(self):
         module = Driver()
         self.assertFormal(module, mode="bmc", depth=4)
         self.assertFormal(module, mode="cover", depth=4)
index ccf003012cbb312d277307ae27721646c3e9457a..950f5ba4ec34589e340e3fc2c675916ca5b94744 100644 (file)
@@ -18,11 +18,10 @@ class ALUInputStage(PipeModBase):
         m = Module()
         comb = m.d.comb
 
-        comb += self.o.op.eq(self.i.op)
 
         a = Signal.like(self.i.a)
 
-        with m.If(self.i.op.invert_a):
+        with m.If(self.i.ctx.op.invert_a):
             comb += a.eq(~self.i.a)
         with m.Else():
             comb += a.eq(self.i.a)
@@ -31,4 +30,6 @@ class ALUInputStage(PipeModBase):
 
         comb += self.o.b.eq(self.i.b)
 
+        comb += self.o.ctx.eq(self.i.ctx)
+
         return m
index cd79abaf38c524348373b798c89daa2274997860..a1bbc7c3c5db18f061891e0ea53a7cac97a85719 100644 (file)
@@ -7,7 +7,6 @@ from ieee754.fpcommon.getop import FPPipeContext
 class IntegerData:
 
     def __init__(self, pspec):
-        self.op = CompALUOpSubset()
         self.ctx = FPPipeContext(pspec)
         self.muxid = self.ctx.muxid
 
@@ -38,7 +37,7 @@ class IntPipeSpec:
     def __init__(self, id_wid=2, op_wid=1):
         self.id_wid = id_wid
         self.op_wid = op_wid
-        self.opkls = CompALUOpSubset
+        self.opkls = lambda _: CompALUOpSubset(name="op")
 
 class ALUPipeSpec(IntPipeSpec):
     def __init__(self, id_wid, op_wid):