From 6398938e6ad67080c978b680377a0a9647045317 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 11 Jan 2023 18:02:45 +0100
Subject: [PATCH] Enable yosys sim support for clock signals in hierarchical
 designs

---
 sbysrc/sby_core.py | 5 ++++-
 sbysrc/sby_sim.py  | 5 ++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index c91561f..f0fcf29 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -989,7 +989,7 @@ class SbyTask(SbyConfig):
                     print("async2sync", file=f)
                     print("chformal -assume -early", file=f)
                 print("opt_clean", file=f)
-                print("formalff -setundef -clk2ff -ff2anyinit", file=f)
+                print("formalff -setundef -clk2ff -ff2anyinit -hierarchy", file=f)
                 if self.opt_mode in ["bmc", "prove"]:
                     print("chformal -live -fair -cover -remove", file=f)
                 if self.opt_mode == "cover":
@@ -1051,6 +1051,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("formalff -assume", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
                     print("formalff -setundef -clk2ff -ff2anyinit", file=f)
@@ -1083,6 +1084,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("formalff -assume", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
                     print("formalff -setundef -clk2ff -ff2anyinit", file=f)
@@ -1117,6 +1119,7 @@ class SbyTask(SbyConfig):
                 print(f"# running in {self.workdir}/model/", file=f)
                 print("read_ilang design_prep.il", file=f)
                 print("hierarchy -simcheck", file=f)
+                print("formalff -assume", file=f)
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 print("setattr -unset keep", file=f)
diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py
index dee99de..0025ed8 100644
--- a/sbysrc/sby_sim.py
+++ b/sbysrc/sby_sim.py
@@ -63,7 +63,10 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()
 
         for assertion in summary["assertions"]:
             if task.design:
-                prop = task.design.properties_by_path[tuple(assertion["path"])]
+                try:
+                    prop = task.design.properties_by_path[tuple(assertion["path"])]
+                except KeyError:
+                    prop = None
             else:
                 prop = None