mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-10 07:10:54 +00:00
Code Activity

Reapply "Remove asserts during cover mode"

Browse source 
This reverts commit 205245c827.
This commit is contained in:
Krystine Sherwin 2025-07-02 18:00:28 +12:00
parent 205245c827
commit aa7d8ab4ce
No known key found for this signature in database
3 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_core.py
View file

@ -1020,7 +1020,7 @@ class SbyTask(SbyConfig):
if self.opt_mode in ["bmc", "prove"]: if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f) print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover": 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": if self.opt_mode == "live":
print("chformal -assert2assume", file=f) print("chformal -assert2assume", file=f)
print("chformal -cover -remove", file=f) print("chformal -cover -remove", file=f)

3
tests/unsorted/mixed.sby
View file

@ -8,6 +8,9 @@ cover: mode cover
bmc: mode bmc bmc: mode bmc
bmc: depth 1 bmc: depth 1
cover: expect pass
~cover: expect fail
[engines] [engines]
cover: btor btormc cover: btor btormc
btormc: btor btormc btormc: btor btormc

2
tests/unsorted/mixed.v
View file

@ -3,7 +3,7 @@ module test (input CP, CN, input A, B, output reg XP, XN);
always @* begin always @* begin
assume (A || B); assume (A || B);
assume (!A || !B); assume (!A || !B);
assert (A != B); assert (A == B);
cover (counter == 3 && A); cover (counter == 3 && A);
cover (counter == 3 && B); cover (counter == 3 && B);
end end