From: Cesar Strauss <cestrauss@gmail.com>
Date: Fri, 28 Oct 2022 12:56:41 +0000 (-0300)
Subject: Check cover and bmc in separate sub-tests
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07ed6f02358197e56dea787fa22bd0bc8934f231;p=soc.git

Check cover and bmc in separate sub-tests

This allows generating a bmc trace even if cover failed.
---

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index 39cad470..6364a515 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -175,9 +175,12 @@ class CompALUMultiTestCase(FHDLTestCase):
                           & (cnt_alu_read == 1)
                           & (cnt_masked_read[0] == 1)
                           & (cnt_masked_read[1] == 1))
-        self.assertFormal(m, mode="cover", depth=10)
+        with self.subTest("cover"):
+            self.assertFormal(m, mode="cover", depth=10)
+
         # Check assertions
-        self.assertFormal(m, mode="bmc", depth=10)
+        with self.subTest("bmc"):
+            self.assertFormal(m, mode="bmc", depth=10)
 
 
 if __name__ == "__main__":