From 07ed6f02358197e56dea787fa22bd0bc8934f231 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Fri, 28 Oct 2022 09:56:41 -0300 Subject: [PATCH] Check cover and bmc in separate sub-tests This allows generating a bmc trace even if cover failed. --- src/soc/experiment/formal/proof_compalu_multi.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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__": -- 2.30.2