diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 6f9c09c..7bc95b3 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -198,6 +198,9 @@ options are: | | | indicated in SBY's log output). | | | | Values: ``on``, ``off``. Default: ``on`` | +-------------------+------------+---------------------------------------------------------+ +| ``cover_assert`` | ``cover`` | Check for assertion properties during ``cover`` mode. | +| | | Values: ``on``, ``off``. Default: ``on`` | ++-------------------+------------+---------------------------------------------------------+ Engines section --------------- diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index e502fe8..6e14d6d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1020,7 +1020,10 @@ class SbyTask(SbyConfig): if self.opt_mode in ["bmc", "prove"]: print("chformal -live -fair -cover -remove", file=f) if self.opt_mode == "cover": - print("chformal -live -fair -assert -remove", file=f) + if self.opt_cover_assert: + print("chformal -live -fair -remove", file=f) + else: + print("chformal -live -fair -assert -remove", file=f) if self.opt_mode == "live": print("chformal -assert2assume", file=f) print("chformal -cover -remove", file=f) @@ -1294,6 +1297,9 @@ class SbyTask(SbyConfig): self.handle_bool_option("skip_prep", False) self.handle_bool_option("assume_early", True) + + if self.opt_mode == "cover": + self.handle_bool_option("cover_assert", False) def setup_status_db(self, status_path=None): if hasattr(self, 'status_db'): diff --git a/tests/junit/junit_cover.sby b/tests/junit/junit_cover.sby index 53747ba..f853d16 100644 --- a/tests/junit/junit_cover.sby +++ b/tests/junit/junit_cover.sby @@ -7,6 +7,7 @@ preunsat [options] mode cover depth 1 +cover_assert on pass: expect pass fail: expect fail