Merge pull request #298 from YosysHQ/george/smtbmc_paths

smtbmc: match on full property paths instead of just names

sbysrc/sby_design.py

@@ -139,32 +139,26 @@ def __iter__(self):
     def get_property_list(self):
         return [p for p in self if p.type != p.Type.ASSUME]
 
-    def find_property(self, hierarchy, location):
-        # FIXME: use that RE that works with escaped paths from https://stackoverflow.com/questions/46207665/regex-pattern-to-split-verilog-path-in-different-instances-using-python
-        path = hierarchy.split('.')
-        mod = path.pop(0)
-        if self.name != mod:
-            raise ValueError(f"{self.name} is not the first module in hierarchical path {hierarchy}.")
-        try:
-            mod_hier = self
-            while path:
-                mod = path.pop(0)
-                mod_hier = mod_hier.submodules[mod]
-        except KeyError:
-            raise KeyError(f"Could not find {hierarchy} in design hierarchy!")
-        try:
-            prop = next(p for p in mod_hier.properties if location in p.location)
-        except StopIteration:
-            raise KeyError(f"Could not find assert at {location} in properties list!")
-        return prop
-
-    def find_property_by_cellname(self, cell_name, trans_dict=dict()):
+    def find_property(self, path, cell_name, trans_dict=dict()):
         # backends may need to mangle names irreversibly, so allow applying
         # the same transformation here
-        for prop in self:
-            if cell_name == prop.name.translate(str.maketrans(trans_dict)):
-                return prop
-        raise KeyError(f"No such property: {cell_name}")
+        trans = str.maketrans(trans_dict)
+        path_iter = iter(path)
+
+        mod = next(path_iter).translate(trans)
+        if self.name != mod:
+            raise ValueError(f"{self.name} is not the first module in hierarchical path {pretty_path(path)}.")
+
+        mod_hier = self
+        for mod in path_iter:
+            mod_hier = next((v for k, v in mod_hier.submodules.items() if mod == k.translate(trans)), None)
+            if not mod_hier:
+                raise KeyError(f"Could not find {pretty_path(path)} in design hierarchy!")
+
+        prop = next((p for p in mod_hier.properties if cell_name == p.name.translate(trans)), None)
+        if not prop:
+            raise KeyError(f"Could not find property {cell_name} at location {pretty_print(path)} in properties list!")
+        return prop
 
 
 @dataclass

sbysrc/sby_engine_aiger.py

@@ -202,6 +202,11 @@ def output_callback2(line):
 
             smt2_trans = {'\\':'/', '|':'/'}
 
+            def parse_mod_path(path_string):
+                # Match a path with . as delimiter, allowing escaped tokens in
+                # verilog `\name ` format
+                return [m[1] or m[0] for m in re.findall(r"(\\([^ ]*) |[^\.]+)(?:\.|$)", path_string)]
+
             match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
             if match:
                 current_step = int(match[1])
@@ -213,10 +218,11 @@ def output_callback2(line):
             match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
             if match: proc2_status = "PASS"
 
-            match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
+            match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line)
             if match:
+                path = parse_mod_path(match[1])
                 cell_name = match[3] or match[2]
-                prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+                prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
                 prop.status = "FAIL"
                 task.status_db.set_task_property_status(prop, data=dict(source="aigsmt", engine=f"engine_{engine_idx}"))
                 last_prop.append(prop)

sbysrc/sby_engine_smtbmc.py

@@ -203,6 +203,11 @@ def output_callback(line):
 
         smt2_trans = {'\\':'/', '|':'/'}
 
+        def parse_mod_path(path_string):
+            # Match a path with . as delimiter, allowing escaped tokens in
+            # verilog `\name ` format
+            return [m[1] or m[0] for m in re.findall(r"(\\([^ ]*) |[^\.]+)(?:\.|$)", path_string)]
+
         match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
         if match:
             current_step = int(match[1])
@@ -228,19 +233,21 @@ def output_callback(line):
             proc_status = "ERROR"
             return line
 
-        match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
+        match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line)
         if match:
+            path = parse_mod_path(match[1])
             cell_name = match[3] or match[2]
-            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
             task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
             last_prop.append(prop)
             return line
 
-        match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+)(?: \((\S+)\))? in step \d+\.", line)
+        match = re.match(r"^## [0-9: ]+ Reached cover statement in step \d+ at ([^:]+): (\S+)(?: \((\S+)\))?", line)
         if match:
-            cell_name = match[2] or match[1]
-            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            path = parse_mod_path(match[1])
+            cell_name = match[3] or match[2]
+            prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
             task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
             last_prop.append(prop)
@@ -268,10 +275,11 @@ def output_callback(line):
                 tracefile = match[1]
                 pending_sim = tracefile
 
-        match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\)\.", line)
+        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, trans_dict=smt2_trans)
+            path = parse_mod_path(match[1])
+            cell_name = match[3] or match[2]
+            prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
             task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))