From: Michael Nolan <mtnolan2640@gmail.com>
Date: Sun, 10 May 2020 16:26:27 +0000 (-0400)
Subject: Reduce BMC depth on proof_main_stage.py
X-Git-Tag: div_pipeline~1298
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8567960f133b3da7a4264706398ef9e9da6b813;p=soc.git

Reduce BMC depth on proof_main_stage.py
---

diff --git a/src/soc/alu/formal/proof_main_stage.py b/src/soc/alu/formal/proof_main_stage.py
index df73815b..3ce8f19a 100644
--- a/src/soc/alu/formal/proof_main_stage.py
+++ b/src/soc/alu/formal/proof_main_stage.py
@@ -100,8 +100,8 @@ class Driver(Elaboratable):
 class ALUTestCase(FHDLTestCase):
     def test_formal(self):
         module = Driver()
-        self.assertFormal(module, mode="bmc", depth=4)
-        self.assertFormal(module, mode="cover", depth=4)
+        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=[])