diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c181c18..e502fe8 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 -remove", file=f) + print("chformal -live -fair -assert -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 2d9467e..4948af0 100644 --- a/tests/unsorted/mixed.sby +++ b/tests/unsorted/mixed.sby @@ -8,6 +8,9 @@ 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 26bf3c9..16e1228 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