From: N. Engelhardt <nak@yosyshq.com>
Date: Fri, 18 Mar 2022 15:36:41 +0000 (+0100)
Subject: translate backslashes in cell names the same way as smt2 backend does
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5dc7fc9a4d7eda59ce49d7553c48603d22a40467;p=SymbiYosys.git

translate backslashes in cell names the same way as smt2 backend does
---

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index 98a57f1..6dfbaec 100644
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -91,11 +91,13 @@ class SbyModule:
             raise KeyError(f"Could not find assert at {location} in properties list!")
         return prop
 
-    def find_property_by_cellname(self, cell_name):
+    def find_property_by_cellname(self, cell_name, trans_dict=dict()):
+        # backends may need to mangle names irreversibly, so allow applying
+        # the same transformation here
         for prop in self:
-            if prop.name == cell_name:
+            if cell_name == prop.name.translate(str.maketrans(trans_dict)):
                 return prop
-        raise KeyError(f"No such property: {cell_name}")
+        raise KeyError(f"No such property: {smt2_name}")
 
 def design_hierarchy(filename):
     design_json = json.load(filename)
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 492e2a5..ab0c7e5 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -160,6 +160,7 @@ def run(mode, task, engine_idx, engine):
     def output_callback(line):
         nonlocal proc_status
         nonlocal last_prop
+        smt2_trans = {'\\':'/', '|':'/'}
 
         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
         if match:
@@ -184,7 +185,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
         if match:
             cell_name = match[3]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
             last_prop = prop
             return line
@@ -192,7 +193,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
         if match:
             cell_name = match[2]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
             last_prop = prop
             return line
@@ -206,7 +207,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
         if match:
             cell_name = match[2]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
 
         return line
diff --git a/tests/submod_props.sby b/tests/submod_props.sby
index 93abc9c..9933676 100644
--- a/tests/submod_props.sby
+++ b/tests/submod_props.sby
@@ -1,10 +1,12 @@
 [tasks]
 bmc
 cover
+flatten
 
 [options]
 bmc: mode bmc
 cover: mode cover
+flatten: mode bmc
 
 expect fail
 
@@ -14,6 +16,7 @@ smtbmc boolector
 [script]
 read -sv test.sv
 prep -top top
+flatten: flatten
 
 [file test.sv]
 module test(input foo);