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 39cad4706b72ae88c263225925739d48b1035ee5..6364a5151e2447bc20fa6bee69845ac284f53704 100644 (file)
--- 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__":