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

@@ -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: aiw2yw doesn't know what to do with the latches
-            #TODO: figure out .ywa
-            # Going via btor seems to lose the seqs, not sure how important they are
             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
 

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}"))

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<type>[cil])(?P<input>\d+) (?P<path>.*?)(\[(?P<offset>\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())