diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index d93d17da..185ed449 100644 --- a/sbysrc/sby_design.py +++ b/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 diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 934269ab..f18e35d8 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/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) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 5fb0b898..24ea00e8 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/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}"))