From 10332e8e74ad30fe4360e7796efb56cc426947ea Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:00 +1300 Subject: [PATCH] btor2aiger: It kinda works? - Add `btor2aig_yw.py` to wrap btor2aiger calls, splitting the symbol map into a `.aim` file and building (and approximation of) the `.ywa` file. - Currently not tracking asserts/assumes in the `.ywa`, and yosys-witness isn't the biggest fan of the btor2aiger style of unitialised latches. As such, the latches are declared but the `.yw` output doesn't do anything with them so it's incomplete. But the vcd output seems fine (for `vcd_sim=on|off`). - Add a try/except to catch property matching with an incomplete property list. - Add `-x` flag to `write_btor` call since aiw2yw gets confused without them. - Includes some TODO reminders for me to fix things, but as far as I can tell it is working. --- sbysrc/sby_core.py | 10 +-- sbysrc/sby_engine_abc.py | 10 ++- tools/btor2aig_yw/btor2aig_yw.py | 118 +++++++++++++++++++++++++++++++ 3 files changed, 131 insertions(+), 7 deletions(-) create mode 100644 tools/btor2aig_yw/btor2aig_yw.py diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 4bfd53e..c56fe63 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1137,7 +1137,8 @@ class SbyTask(SbyConfig): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + #TODO: put -x in a conditional + print("write_btor -x {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) proc = SbyProc( @@ -1151,15 +1152,14 @@ class SbyTask(SbyConfig): return [proc] if model_name == "aig" and self.opt_btor_aig: - #TODO: split .aim from .aig? - #TODO: figure out .ywa - # Going via btor seems to lose the seqs, not sure how important they are + #TODO: aiw2yw doesn't know what to do with the latches btor_model = "btor_nomem" proc = SbyProc( self, "btor_aig", self.model(btor_model), - f"""cd {self.workdir}/model; btor2aiger design_{btor_model}.btor > design_aiger.aig""" + #TODO: fix hardcoded path + f"cd {self.workdir}/model; python3 ~/sby/tools/btor2aig_yw/btor2aig_yw.py design_{btor_model}.btor" ) proc.checkretcode = True diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 1fabe6f..bd9d51d 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -166,7 +166,10 @@ def run(mode, task, engine_idx, engine): match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line) if match: output = int(match[1]) - prop = aiger_props[output] + try: + prop = aiger_props[output] + except IndexError: + prop = None if prop: prop.status = "FAIL" task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) @@ -185,7 +188,10 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line) if match: output = int(match[1]) - prop = aiger_props[output] + try: + prop = aiger_props[output] + except IndexError: + prop = None if prop: prop.status = "PASS" task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py new file mode 100644 index 0000000..841383c --- /dev/null +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -0,0 +1,118 @@ +from __future__ import annotations + +import argparse +import asyncio +import json +import re +from pathlib import Path + +def arg_parser(): + parser = argparse.ArgumentParser() + + parser.add_argument( + "btor_file", + type=Path + ) + + parser.add_argument( + "-d", "--dest", + dest="dest", + required=False, + type=Path + ) + + return parser + +async def main() -> None: + args = arg_parser().parse_args() + + work_dir: Path = args.dest or Path() + + proc = await asyncio.create_subprocess_shell( + f"btor2aiger {args.btor_file}", + stdout=asyncio.subprocess.PIPE + ) + + data = True + + # output aig + aig_file = work_dir / "design_aiger.aig" + aigf = open(aig_file, mode="wb") + data = await proc.stdout.readline() + aig_header = data.decode() + while data: + aigf.write(data) + data = await proc.stdout.readline() + if b'i0' in data: + break + end_pos = data.find(b'i0') + aigf.write(data[:end_pos]) + aigf.close() + + # initialize yw aiger map + aig_MILOA = aig_header.split() + ywa = { + "version": "Yosys Witness Aiger map", + "generator": "btor2aig_yw.py", + "latch_count": int(aig_MILOA[3]), + "input_count": int(aig_MILOA[2]), + "clocks": [], + "inputs": [], + "seqs": [], + "inits": [], + "latches": [], + "asserts": [], + "assumes": [] + } + + # output aim & build ywa + aim_file = work_dir / "design_aiger.aim" + aimf = open(aim_file, mode="w") + data = data[end_pos:] + while data: + # decode data + string = data.decode().rstrip() + pattern = r"(?P[cil])(?P\d+) (?P.*?)(\[(?P\d+)\])?$" + m = re.match(pattern, string) + md = m.groupdict() + if md['type'] == 'i': + md['type'] = 'input' + elif md['type'] == 'c': + md['type'] = 'clk' + elif md['type'] == 'l': + md['type'] = 'latch' + else: + raise ValueError(f"Unknown type identifier {md['type']!r}") + for k in ['input', 'offset']: + if md[k]: + md[k] = int(md[k]) + else: + md[k] = 0 + + # output to aim + if md['type'] in ['input', 'latch']: + print("{type} {input} {offset} {path}".format(**md), file=aimf) + + # update ywa + md_type = md.pop('type') + if md['path'][0] == '$': + md['path'] = [md['path']] + else: + md['path'] = [f"\\{s}" for s in md['path'].replace('[','.[').split('.')] + if md_type == 'clk': + md['edge'] = "posedge" # always? + ywa['clocks'].append(md) + elif md_type == 'input': + ywa['inputs'].append(md) + elif md_type == 'latch': + ywa['latches'].append(md) + + # get next line + data = await proc.stdout.readline() + aimf.close() + + with open(work_dir / "design_aiger.ywa", mode="w") as f: + json.dump(ywa, f, indent=2) + +if __name__ == "__main__": + asyncio.run(main())