From 99e704e6cb76663b7cdaaf07e5cf0766d434e51a 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: Get assertions from .btor file

Assertions show up in the .btor file as 'bad' statements, assuming btor2aiger maintains the same order this should get us the list of assertions in the order they appear in the .aig file.
---
 tools/btor2aig_yw/btor2aig_yw.py | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py
index 841383c..3fe4f3a 100644
--- a/tools/btor2aig_yw/btor2aig_yw.py
+++ b/tools/btor2aig_yw/btor2aig_yw.py
@@ -23,6 +23,13 @@ def arg_parser():
 
     return parser
 
+def fix_path(path: str) -> list[str]:
+    if path[0] == '$':
+        fixed = [path]
+    else:
+        fixed = [f"\\{s}" for s in path.replace('[','.[').split('.')]
+    return fixed
+
 async def main() -> None:
     args = arg_parser().parse_args()
 
@@ -95,10 +102,7 @@ async def main() -> None:
 
         # 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('.')]
+        md['path'] = fix_path(md['path'])
         if md_type == 'clk':
             md['edge'] = "posedge" # always?
             ywa['clocks'].append(md)
@@ -111,6 +115,17 @@ 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(work_dir / "design_aiger.ywa", mode="w") as f:
         json.dump(ywa, f, indent=2)