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 @@ def instance_hierarchy_error_callback(retcode):
  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 @@ def instance_hierarchy_error_callback(retcode):
  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
 

sbysrc/sby_engine_abc.py

@@ -166,7 +166,10 @@ def output_callback(line):
  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 output_callback(line):
  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())