From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sun, 24 May 2020 12:03:53 +0000 (+0100)
Subject: error in alu output stage formal proof setup
X-Git-Tag: div_pipeline~889
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c499d7c521c0fb916254d51df61f583b2d1f56d;p=soc.git

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 ff838d91..f03196e4 100644
--- 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):