From 08079a435ba6136de2a329b35d39b500be825673 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 30 Jan 2017 11:39:48 +0100 Subject: [PATCH] Fix "abc bmc3" engine for small state spaces --- sbysrc/sby_bmc.py | 3 +++ 1 file changed, 3 insertions(+) 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" -- 2.30.2