diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index e502fe8..c181c18 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1020,7 +1020,7 @@ 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) + print("chformal -live -fair -remove", file=f) if self.opt_mode == "live": print("chformal -assert2assume", file=f) print("chformal -cover -remove", file=f) diff --git a/tests/unsorted/mixed.sby b/tests/unsorted/mixed.sby index 4948af0..2d9467e 100644 --- a/tests/unsorted/mixed.sby +++ b/tests/unsorted/mixed.sby @@ -8,9 +8,6 @@ cover: mode cover bmc: mode bmc bmc: depth 1 -cover: expect pass -~cover: expect fail - [engines] cover: btor btormc btormc: btor btormc diff --git a/tests/unsorted/mixed.v b/tests/unsorted/mixed.v index 16e1228..26bf3c9 100644 --- a/tests/unsorted/mixed.v +++ b/tests/unsorted/mixed.v @@ -3,7 +3,7 @@ module test (input CP, CN, input A, B, output reg XP, XN); always @* begin assume (A || B); assume (!A || !B); - assert (A == B); + assert (A != B); cover (counter == 3 && A); cover (counter == 3 && B); end