From 9168b0163bfe3e9bffca915bdae05d27ffc5f992 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Sun, 6 Feb 2022 09:15:44 +0100 Subject: [PATCH] handle status of cover properties --- sbysrc/sby.py | 17 +++++++++-------- sbysrc/sby_design.py | 23 +++++++++++++++++------ sbysrc/sby_engine_smtbmc.py | 24 +++++++++++++----------- 3 files changed, 39 insertions(+), 25 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 8d6cfc9..ee8f1a3 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -20,7 +20,7 @@ import argparse, os, sys, shutil, tempfile, re ##yosys-sys-path## from sby_core import SbyTask, SbyAbort, process_filename -import time +import time, platform class DictAction(argparse.Action): def __call__(self, parser, namespace, values, option_string=None): @@ -458,7 +458,6 @@ def run_task(taskname): checks = task.design_hierarchy.get_property_list() junit_tests = len(checks) junit_errors = 1 if task.retcode == 16 else 0 - solver_gives_line = task.status == "FAIL" and any(check.status != "UNKNOWN" for check in checks) junit_failures = 0 if junit_errors == 0 and task.retcode != 0: if solver_gives_line: @@ -471,15 +470,17 @@ def run_task(taskname): junit_time = time.strftime('%Y-%m-%dT%H:%M:%S') print(f'', file=f) print(f'', file=f) - #TODO: check with Micko if os.uname().nodename is sane enough in most places - print(f'', file=f) + print(f'', file=f) print(f'', file=f) - print(f'', file=f) + print(f'', file=f) print(f'', file=f) - if solver_gives_line: + if task.precise_prop_status: for check in checks: - print(f'', file=f) # name required - if check.status == "UNKNOWN": + detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"' + print(f'', file=f) # name required + if check.status == "PASS": + pass + elif check.status == "UNKNOWN": print(f'', file=f) elif check.status == "FAIL": print(f'', file=f) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 7551ac7..c0fdb8b 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -63,12 +63,14 @@ class SbyModule: def __repr__(self): return f"SbyModule<{self.name} : {self.type}, submodules={self.submodules}, properties={self.properties}>" - def get_property_list(self): - l = list() - l.extend(self.properties) + def __iter__(self): + for prop in self.properties: + yield prop for submod in self.submodules.values(): - l.extend(submod.get_property_list()) - return l + yield from submod.__iter__() + + 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 @@ -89,6 +91,12 @@ class SbyModule: raise KeyError(f"Could not find assert at {location} in properties list!") return prop + def find_property_by_cellname(self, cell_name): + for prop in self: + if prop.name == cell_name: + return prop + raise KeyError(f"No such property: {cell_name}") + def design_hierarchy(filename): design_json = json.load(filename) def make_mod_hier(instance_name, module_name, hierarchy=""): @@ -121,7 +129,10 @@ def main(): if len(sys.argv) != 2: print(f"""Usage: {sys.argv[0]} design.json""") with open(sys.argv[1]) as f: - print(design_hierarchy(f)) + d = design_hierarchy(f) + print("Design Hierarchy:", d) + for p in d.get_property_list(): + print("Property:", p) if __name__ == '__main__': main() diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index b736e31..e179dd5 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -143,7 +143,7 @@ def run(mode, task, engine_idx, engine): task, procname, task.model(model_name), - f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""", + f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --cellinfo --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""", logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress) ) @@ -181,22 +181,20 @@ def run(mode, task, engine_idx, engine): proc_status = "ERROR" return line - match = re.match(r"^## [0-9: ]+ Assert failed in (([a-z_][a-z0-9$_]*|\\\S*|\.)+): (\S*).*", line) + match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line) if match: - module_path = match[1] - location = match[3] - try: - prop = task.design_hierarchy.find_property(module_path, location) - except KeyError as e: - task.precise_prop_status = False - return line + f" (Warning: {str(e)})" + cell_name = match[3] + prop = task.design_hierarchy.find_property_by_cellname(cell_name) prop.status = "FAIL" last_prop = prop return line - match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) in step \d+.", line) + match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line) if match: - location = match[1] + cell_name = match[2] + prop = task.design_hierarchy.find_property_by_cellname(cell_name) + prop.status = "PASS" + last_prop = prop match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) if match and last_prop: @@ -231,6 +229,10 @@ def run(mode, task, engine_idx, engine): excess_traces += 1 if excess_traces > 0: task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") + elif proc_status == "PASS" and mode == "bmc": + for prop in task.design_hierarchy: + if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": + prop.status = "PASS" task.terminate() -- 2.30.2