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 98a57f132b16c1c733c1234ace39b1e1f450d312..6dfbaecb9dd9dab6dee8975ceb9bd7e85ccb2666 100644 (file)
--- 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 492e2a57f01a248c97ec39cb698bfc1b334c4de5..ab0c7e5f243ca17b43a319b100e73865256ddb3a 100644 (file)
--- 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 93abc9c139d18ca8d8fe07d943e7f63acec99fec..99336767d86772ce4b8452ec1df50935e55950c6 100644 (file)
--- 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);