From c081a8a75463b7a86b27bfbf1ab059945d99a327 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH] btor2aiger: Use asserts and assumes from .ywb file --- sbysrc/sby_core.py | 2 +- tools/btor2aig_yw/btor2aig_yw.py | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f2fc55b..99631f5 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1159,7 +1159,7 @@ class SbyTask(SbyConfig): self, "btor_aig", self.model(btor_model), - f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor" + f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor design_btor.ywb" ) proc.checkretcode = True diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 98ad124..c8c727d 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -15,6 +15,11 @@ def arg_parser(): type=Path ) + parser.add_argument( + "ywb_file", + type=Path + ) + parser.add_argument( "-d", "--dest", dest="dest", @@ -118,15 +123,10 @@ async def main() -> None: data = await proc.stdout.readline() aimf.close() - # find assertions by looking for 'bad' statements in the btor - with open(args.btor_file, mode='r') as f: - data = f.readline() - while data: - if "bad" in data: - m = re.match(r"^\d+ bad \d+ (\S+)", data) - path = fix_path(m.group(1)) - ywa['asserts'].append(path) - data = f.readline() + with open(args.ywb_file, mode='r') as f: + data = json.load(f) + ywa['asserts'].extend(data['asserts']) + ywa['assumes'].extend(data['assumes']) with open(work_dir / "design_aiger.ywa", mode="w") as f: