cleanup logical pipe formal proof

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 456ff815348a80f243bcdeddf1d51d1fc78a5092..9497dd1b083fc544005d02a7ff0ac49acf693594 100644 (file)
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -38,14 +38,12 @@ class Driver(Elaboratable):
         comb = m.d.comb
 
         rec = CompALUOpSubset()
         comb = m.d.comb
 
         rec = CompALUOpSubset()

-        recwidth = 0

         # Setup random inputs for dut.op
         for p in rec.ports():
             width = p.width
         # Setup random inputs for dut.op
         for p in rec.ports():
             width = p.width

-            recwidth += width

             comb += p.eq(AnyConst(width))
 
             comb += p.eq(AnyConst(width))
 

-        pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
+        pspec = ALUPipeSpec(id_wid=2)

         m.submodules.dut = dut = LogicalMainStage(pspec)
 
         # convenience variables
         m.submodules.dut = dut = LogicalMainStage(pspec)
 
         # convenience variables


@@ -53,14 +51,13 @@ class Driver(Elaboratable):
         b = dut.i.b
         carry_in = dut.i.xer_ca[0]
         carry_in32 = dut.i.xer_ca[1]
         b = dut.i.b
         carry_in = dut.i.xer_ca[0]
         carry_in32 = dut.i.xer_ca[1]

-        so_in = dut.i.xer_so

         o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
                  b.eq(AnyConst(64)),
                  carry_in.eq(AnyConst(0b11)),
         o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
                  b.eq(AnyConst(64)),
                  carry_in.eq(AnyConst(0b11)),

-                 so_in.eq(AnyConst(1))]
+                 ]

 
         comb += dut.i.ctx.op.eq(rec)
 
 
         comb += dut.i.ctx.op.eq(rec)