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