Allow the formal engine to perform a same-cycle result in the ALU

[soc.git] / src / soc / fu / alu / formal / proof_main_stage.py

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index a5e8e12fd7afdcb3f71336e72471f862fb99a543..de8dc54f1c82ea18eb768e40ec183fab119e5049 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -16,7 +16,7 @@ from nmigen.cli import rtlil
 from soc.fu.alu.main_stage import ALUMainStage
 from soc.fu.alu.pipe_data import ALUPipeSpec
 from soc.fu.alu.alu_input_record import CompALUOpSubset
-from soc.decoder.power_enums import MicrOp
+from openpower.decoder.power_enums import MicrOp
 import unittest
 
 
@@ -37,20 +37,20 @@ class Driver(Elaboratable):
             width = p.width
             comb += p.eq(AnyConst(width))
 
-        pspec = ALUPipeSpec(id_wid=2)
+        pspec = ALUPipeSpec(id_wid=2, parent_pspec=None)
         m.submodules.dut = dut = ALUMainStage(pspec)
 
         # convenience variables
         a = dut.i.a
         b = dut.i.b
         ca_in = dut.i.xer_ca[0]   # CA carry in
-        ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
+        ca32_in = dut.i.xer_ca[1]  # CA32 carry in 32
         so_in = dut.i.xer_so      # SO sticky overflow
 
         ca_o = dut.o.xer_ca.data[0]   # CA carry out
-        ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
+        ca32_o = dut.o.xer_ca.data[1]  # CA32 carry out32
         ov_o = dut.o.xer_ov.data[0]   # OV overflow
-        ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
+        ov32_o = dut.o.xer_ov.data[1]  # OV32 overflow32
         o = dut.o.o.data
 
         # setup random inputs
@@ -143,6 +143,7 @@ class ALUTestCase(FHDLTestCase):
         module = Driver()
         self.assertFormal(module, mode="bmc", depth=2)
         self.assertFormal(module, mode="cover", depth=2)
+
     def test_ilang(self):
         dut = Driver()
         vl = rtlil.convert(dut, ports=[])