error in alu output stage formal proof setup

diff --git a/src/soc/fu/alu/formal/proof_output_stage.py b/src/soc/fu/alu/formal/proof_output_stage.py
index ff838d9192aa1a8146dab49cf0abc5126a1c71f3..f03196e4cdde251b6d9e0cd781204acff52f2c54 100644 (file)
--- a/src/soc/fu/alu/formal/proof_output_stage.py
+++ b/src/soc/fu/alu/formal/proof_output_stage.py
@@ -32,7 +32,7 @@ class Driver(Elaboratable):
             recwidth += width
             comb += p.eq(AnyConst(width))
 
-        pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
+        pspec = ALUPipeSpec(id_wid=2)
         m.submodules.dut = dut = ALUOutputStage(pspec)
 
         o = Signal(64)
@@ -88,7 +88,6 @@ class Driver(Elaboratable):
             with m.Else():
                 comb += Assert(cr_out[3] == 1)
 
-
         # Assert that op gets copied from the input to output
         for p in rec.ports():
             name = p.name
@@ -96,7 +95,6 @@ class Driver(Elaboratable):
             dut_sig = getattr(dut.o.ctx.op, name)
             comb += Assert(dut_sig == rec_sig)
 
-
         return m
 
 class GTCombinerTestCase(FHDLTestCase):