diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f2fc55ba..99631f55 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1159,7 +1159,7 @@ def instance_hierarchy_error_callback(retcode): 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 98ad1240..c8c727d2 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: