From db782815f2c79b8fe5d2bd39d3948aaec0b66397 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 30 Sep 2025 10:31:40 +1300 Subject: [PATCH] More tests without properties Used `sby --autotune` to find other engines which fail (though there aren't any other exceptions that I could find). Parse errors from `abc bmc3` and `abc sim3` instead of returning UNKNOWN. --- sbysrc/sby_engine_abc.py | 3 +++ tests/unsorted/no_props.sby | 19 ++++++++++++++++--- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 5bcb66f..42dbd0a 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -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 index afeeeb2..6fce5e8 100644 --- a/tests/unsorted/no_props.sby +++ b/tests/unsorted/no_props.sby @@ -1,13 +1,26 @@ [tasks] -abc -abc_keepgoing +abc prove +abc_keepgoing prove + +# "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] -mode prove +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 +abc_bmc3: abc bmc3 +abc_sim3: abc sim3 [script] read -sv test.sv