From 1cf27e7c315daa6019a9a6398a9827cfddf9c84b Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 27 Jan 2022 13:41:07 +0100 Subject: [PATCH] parse solver location output for assert failures (cover not functional yet) --- sbysrc/sby.py | 2 +- sbysrc/sby_core.py | 14 ++++++++------ sbysrc/sby_design.py | 29 +++++++++++++++++++++++++++-- sbysrc/sby_engine_smtbmc.py | 25 +++++++++++++++++++++++++ tests/submod_props.sby | 30 ++++++++++++++++++++++++++++++ 5 files changed, 91 insertions(+), 9 deletions(-) create mode 100644 tests/submod_props.sby diff --git a/sbysrc/sby.py b/sbysrc/sby.py index f3b78ea..8d6cfc9 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -478,7 +478,7 @@ def run_task(taskname): print(f'', file=f) if solver_gives_line: for check in checks: - print(f'', file=f) # name required + print(f'', file=f) # name required if check.status == "UNKNOWN": print(f'', file=f) elif check.status == "FAIL": diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 840f215..ec4e0a1 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -222,8 +222,9 @@ class SbyTask: self.reusedir = reusedir self.status = "UNKNOWN" self.total_time = 0 - self.expect = [] + self.expect = list() self.design_hierarchy = None + self.precise_prop_status = False yosys_program_prefix = "" ##yosys-program-prefix## self.exe_paths = { @@ -371,6 +372,9 @@ class SbyTask: print(f"# running in {self.workdir}/src/", file=f) for cmd in self.script: print(cmd, file=f) + # assumptions at this point: hierarchy has been run and a top module has been designated + print("hierarchy -simcheck", file=f) + print(f"""write_json ../model/design.json""", file=f) if model_name == "base": print("memory_nordff", file=f) else: @@ -392,8 +396,6 @@ class SbyTask: print("opt -keepdc -fast", file=f) print("check", file=f) print("hierarchy -simcheck", file=f) - # FIXME: can using design and design_nomem in the same task happen? - print(f"""write_json ../model/design{"" if model_name == "base" else "_nomem"}.json""", file=f) print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f) proc = SbyProc( @@ -407,9 +409,9 @@ class SbyTask: def instance_hierarchy_callback(retcode): assert retcode == 0 - assert self.design_hierarchy == None # verify this assumption - with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f: - self.design_hierarchy = design_hierarchy(f) + if self.design_hierarchy == None: + with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f: + self.design_hierarchy = design_hierarchy(f) proc.exit_callback = instance_hierarchy_callback diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 79c4ddd..7551ac7 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -28,7 +28,7 @@ class SbyProperty: COVER = auto() LIVE = auto() - def __repr__(self): + def __str__(self): return self.name @classmethod @@ -50,6 +50,9 @@ class SbyProperty: status: str = field(default="UNKNOWN") tracefile: str = field(default="") + def __repr__(self): + return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\"" + @dataclass class SbyModule: name: str @@ -57,13 +60,35 @@ class SbyModule: submodules: dict = field(default_factory=dict) properties: list = field(default_factory=list) + 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) - for submod in self.submodules: + for submod in self.submodules.values(): l.extend(submod.get_property_list()) return l + 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 design_hierarchy(filename): design_json = json.load(filename) def make_mod_hier(instance_name, module_name, hierarchy=""): diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index da2e31c..b736e31 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -32,6 +32,7 @@ def run(mode, task, engine_idx, engine): basecase_only = False induction_only = False random_seed = None + task.precise_prop_status = True opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="]) @@ -154,9 +155,11 @@ def run(mode, task, engine_idx, engine): task.induction_procs.append(proc) proc_status = None + last_prop = None def output_callback(line): nonlocal proc_status + nonlocal last_prop match = re.match(r"^## [0-9: ]+ Status: FAILED", line) if match: @@ -178,6 +181,28 @@ 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) + 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)})" + prop.status = "FAIL" + last_prop = prop + return line + + match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) in step \d+.", line) + if match: + location = match[1] + + match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) + if match and last_prop: + last_prop.tracefile = match[1] + last_prop = None + return line def exit_callback(retcode): diff --git a/tests/submod_props.sby b/tests/submod_props.sby new file mode 100644 index 0000000..33a3a00 --- /dev/null +++ b/tests/submod_props.sby @@ -0,0 +1,30 @@ +[tasks] +bmc +cover + +[options] +bmc: mode bmc +cover: mode cover + +expect fail + +[engines] +smtbmc boolector + +[script] +read_verilog -sv test.sv +prep -top top + +[file test.sv] +module test(input foo); +always @* assert(foo); +always @* assert(!foo); +always @* cover(foo); +always @* cover(!foo); +endmodule + +module top(); +test test_i ( +.foo(1'b1) +); +endmodule -- 2.30.2