mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-11-29 02:09:52 +00:00
Code Activity

Fix abc crash when aiger_props is empty

Browse source 
Includes test reproducer from #338, modified to also test `abc --keep-going pdr`.
This commit is contained in:
Krystine Sherwin 2025-09-30 10:26:36 +13:00
parent 12380801e3
commit c06d8682cd
No known key found for this signature in database
2 changed files with 23 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
sbysrc/sby_engine_abc.py
View file

@ -203,7 +203,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line) match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line)
if match: if match:
output = int(match[1]) output = int(match[1])
prop = aiger_props[output] prop = aiger_props[output] if aiger_props else None
if prop: if prop:
prop.status = "PASS" prop.status = "PASS"
task.summary.add_event( task.summary.add_event(
@ -232,7 +232,7 @@ def run(mode, task, engine_idx, engine):
disproved_count = int(match[3]) disproved_count = int(match[3])
undecided_count = int(match[4]) undecided_count = int(match[4])
if ( if (
all_count != len(aiger_props) or (aiger_props and all_count != len(aiger_props)) or
all_count != proved_count + disproved_count + undecided_count or all_count != proved_count + disproved_count + undecided_count or
disproved_count != len(disproved) or disproved_count != len(disproved) or
proved_count != len(proved) proved_count != len(proved)

21
tests/unsorted/no_props.sby Normal file
View file

@ -0,0 +1,21 @@
[tasks]
abc
abc_keepgoing
[options]
mode prove
[engines]
abc: abc pdr
abc_keepgoing: abc --keep-going pdr
[script]
read -sv test.sv
prep -top top
[file test.sv]
module top(input i, output o);
assign o = ~i;
endmodule