From: Cesar Strauss 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__":