From: Clifford Wolf Date: Mon, 30 Jan 2017 10:39:48 +0000 (+0100) Subject: Fix "abc bmc3" engine for small state spaces X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08079a435ba6136de2a329b35d39b500be825673;p=SymbiYosys.git Fix "abc bmc3" engine for small state spaces --- diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py index a0f3d7b..1c146f7 100644 --- a/sbysrc/sby_bmc.py +++ b/sbysrc/sby_bmc.py @@ -94,6 +94,9 @@ def run_abc(job, engine_idx, engine): match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) if match: task_status = "FAIL" + match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line) + if match: task_status = "PASS" + match = re.match(r"^No output asserted in [0-9]+ frames.", line) if match: task_status = "PASS"