From aa7d8ab4ce3b8af8ba8df1d34a50a846792fa69e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 2 Jul 2025 18:00:28 +1200 Subject: [PATCH] Reapply "Remove asserts during cover mode" This reverts commit 205245c827c0c7d2e902c5236a5850661ca6f58e. --- sbysrc/sby_core.py | 2 +- tests/unsorted/mixed.sby | 3 +++ tests/unsorted/mixed.v | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) 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