diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index d8e0189..42dbd0a 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -203,7 +203,7 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line) if match: output = int(match[1]) - prop = aiger_props[output] + prop = aiger_props[output] if aiger_props else None if prop: prop.status = "PASS" task.summary.add_event( @@ -232,7 +232,7 @@ def run(mode, task, engine_idx, engine): disproved_count = int(match[3]) undecided_count = int(match[4]) 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 disproved_count != len(disproved) or proved_count != len(proved) @@ -246,6 +246,9 @@ def run(mode, task, engine_idx, engine): else: proc_status = "FAIL" + match = re.match("Error: (Does not work|Only works) for (sequential|combinational) networks.", line) + if match: proc_status = "ERROR" + return line def exit_callback(retcode): diff --git a/tests/unsorted/no_props.sby b/tests/unsorted/no_props.sby new file mode 100644 index 0000000..f05fc3a --- /dev/null +++ b/tests/unsorted/no_props.sby @@ -0,0 +1,36 @@ +[tasks] +abc prove +abc_keepgoing prove +btor_cover cover + +# "Error: Does not work for combinational networks." +abc_bmc3 bmc error +# "Error: Only works for sequential networks." +abc_sim3 bmc error +# "Property index 0 is greater than the number of properties in file model/design_btor_single.btor (0)" +btor_pono bmc error + +[options] +prove: mode prove +bmc: mode bmc +cover: mode cover +error: expect ERROR + +[engines] +abc: abc pdr +abc_keepgoing: abc --keep-going pdr +btor_pono: btor pono +btor_cover: btor btormc +abc_bmc3: abc bmc3 +abc_sim3: abc sim3 + +[script] +read -sv test.sv +prep -top top + +[file test.sv] +module top(input i, output o); + +assign o = ~i; + +endmodule