From 1eeb6f3f0bbea9af1ae862f0419149d0bc8e483c Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 22 Jan 2024 18:10:00 +0100
Subject: [PATCH 1/2] Delete `$print` cells in the backend flows

They are only useful and supported for the simulation that is run with
the output of the prep flow, not the output of the backend flows.
---
 sbysrc/sby_core.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 8d2fc76..d59ffa1 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1055,6 +1055,7 @@ class SbyTask(SbyConfig):
                 print(f"# running in {self.workdir}/model/", file=f)
                 print(f"""read_ilang design_prep.il""", file=f)
                 print("hierarchy -smtcheck", file=f)
+                print("delete */t:$print", file=f)
                 print("formalff -assume", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
@@ -1088,6 +1089,7 @@ class SbyTask(SbyConfig):
                 print(f"# running in {self.workdir}/model/", file=f)
                 print(f"""read_ilang design_prep.il""", file=f)
                 print("hierarchy -simcheck", file=f)
+                print("delete */t:$print", file=f)
                 print("formalff -assume", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
@@ -1122,6 +1124,7 @@ class SbyTask(SbyConfig):
             with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
                 print(f"# running in {self.workdir}/model/", file=f)
                 print("read_ilang design_prep.il", file=f)
+                print("delete */t:$print", file=f)
                 print("hierarchy -simcheck", file=f)
                 print("formalff -assume", file=f)
                 print("flatten", file=f)

From 881082c9908aa81101fea52c7c8473607cb1b119 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 22 Jan 2024 18:11:16 +0100
Subject: [PATCH 2/2] sby_design: Discover properties represented using
 `$check` cells

---
 sbysrc/sby_design.py | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index 88b6395..a449a9b 100644
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -71,6 +71,18 @@ class SbyProperty:
                 return c.LIVE
             raise ValueError("Unknown property type: " + name)
 
+        @classmethod
+        def from_flavor(c, name):
+            if name == "assume":
+                return c.ASSUME
+            if name == "assert":
+                return c.ASSERT
+            if name == "cover":
+                return c.COVER
+            if name == "live":
+                return c.LIVE
+            raise ValueError("Unknown property type: " + name)
+
     name: str
     path: Tuple[str, ...]
     type: Type
@@ -199,6 +211,20 @@ def design_hierarchy(filename):
                         location=location,
                         hierarchy=sub_hierarchy)
                     mod.properties.append(p)
+            if sort["type"] == "$check":
+                for cell in sort["cells"]:
+                    try:
+                        location = cell["attributes"]["src"]
+                    except KeyError:
+                        location = ""
+                    p = SbyProperty(
+                        name=cell["name"],
+                        path=(*path, *cell_path(cell)),
+                        type=SbyProperty.Type.from_flavor(cell["parameters"]["FLAVOR"]),
+                        location=location,
+                        hierarchy=sub_hierarchy)
+                    mod.properties.append(p)
+
             if sort["type"][0] != '$' or sort["type"].startswith("$paramod"):
                 for cell in sort["cells"]:
                     mod.submodules[cell["name"]] = make_mod_hier(