From 7f3c4137c10c79c671a8f20b8d6b20a16487beee Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 19 Jan 2022 19:34:11 +0100 Subject: [PATCH] create json export and read in properties --- sbysrc/sby.py | 26 +++++------ sbysrc/sby_core.py | 12 +++++ sbysrc/sby_design.py | 102 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 125 insertions(+), 15 deletions(-) create mode 100644 sbysrc/sby_design.py diff --git a/sbysrc/sby.py b/sbysrc/sby.py index c720b22..3d2f583 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -455,18 +455,14 @@ def run_task(taskname): if not my_opt_tmpdir and not setupmode: with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f: - # TODO: create necessary data - # checks: collection of assert/cover statements active in task - # elements: dicts with entries 'type', 'hierarchy', 'location', 'status', 'tracefile' - checks = [ #for testing purposes - {'type':'assert', 'hierarchy':'top.dut.submod1', 'location':'test.v:404', 'status':'unknown', 'tracefile':'/home/user/path/task/engine_0/trace0.vcd'}, - {'type':'assert', 'hierarchy':'top.dut.submod1', 'location':'test.v:412', 'status':'fail', 'tracefile':'/home/user/path/task/engine_0/trace1.vcd'}, - {'type':'cover', 'hierarchy':'top.dut.submod2', 'location':'test3.v:42', 'status':'pass', 'tracefile':'/home/user/path/task/engine_1/trace0.vcd'}, - {'type':'cover', 'hierarchy':'top.dut.submod2', 'location':'test3.v:666', 'status':'error', 'tracefile':'/home/user/path/task/engine_1/trace1.vcd'} - ] + checks = task.design_hierarchy.get_property_list() junit_tests = len(checks) junit_errors = 1 if task.retcode == 16 else 0 - junit_failures = 1 if task.retcode != 0 and junit_errors == 0 else 0 + junit_failures = 0 + if task.retcode != 0 and junit_errors == 0: + for check in checks: + if check.status == "FAIL": + junit_failures += 1 junit_type = "cover" if task.opt_mode == "cover" else "assert" #should this be here or individual for each check? junit_time = time.strftime('%Y-%m-%dT%H:%M:%S') print(f'', file=f) @@ -478,12 +474,12 @@ def run_task(taskname): print(f'', file=f) for check in checks: print(f'', file=f) # name required - if check["status"] == "unknown": + if check.status == "UNKNOWN": print(f'', file=f) - elif check["status"] == "fail": - print(f'', file=f) - elif check["status"] == "error": - print(f'', file=f) # type mandatory, message optional + elif check.status == "FAIL": + print(f'', file=f) + elif check.status == "ERROR": + print(f'', file=f) # type mandatory, message optional print(f'', file=f) print('', end="", file=f) with open(f"{task.workdir}/logfile.txt", "r") as logf: diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f05b31d..840f215 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -23,6 +23,7 @@ import subprocess from shutil import copyfile, copytree, rmtree from select import select from time import time, localtime, sleep +from sby_design import SbyProperty, SbyModule, design_hierarchy all_procs_running = [] @@ -222,6 +223,7 @@ class SbyTask: self.status = "UNKNOWN" self.total_time = 0 self.expect = [] + self.design_hierarchy = None yosys_program_prefix = "" ##yosys-program-prefix## self.exe_paths = { @@ -390,6 +392,8 @@ 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( @@ -401,6 +405,14 @@ class SbyTask: ) proc.checkretcode = True + 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) + + proc.exit_callback = instance_hierarchy_callback + return [proc] if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name): diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py new file mode 100644 index 0000000..79c4ddd --- /dev/null +++ b/sbysrc/sby_design.py @@ -0,0 +1,102 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2022 N. Engelhardt +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import json +from enum import Enum, auto +from dataclasses import dataclass, field + +@dataclass +class SbyProperty: + class Type(Enum): + ASSUME = auto() + ASSERT = auto() + COVER = auto() + LIVE = auto() + + def __repr__(self): + return self.name + + @classmethod + def from_cell(c, name): + if name == "$assume": + return c.ASSUME + if name == "$assert": + return c.ASSERT + if name == "$cover": + return c.COVER + if name == "$live": + return c.LIVE + raise ValueError("Unknown property type: " + name) + + name: str + type: Type + location: str + hierarchy: str + status: str = field(default="UNKNOWN") + tracefile: str = field(default="") + +@dataclass +class SbyModule: + name: str + type: str + submodules: dict = field(default_factory=dict) + properties: list = field(default_factory=list) + + def get_property_list(self): + l = list() + l.extend(self.properties) + for submod in self.submodules: + l.extend(submod.get_property_list()) + return l + +def design_hierarchy(filename): + design_json = json.load(filename) + def make_mod_hier(instance_name, module_name, hierarchy=""): + # print(instance_name,":", module_name) + mod = SbyModule(name=instance_name, type=module_name) + + cells = design_json["modules"][module_name]["cells"] + for cell_name, cell in cells.items(): + if cell["type"][0] != '$': + mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=f"{hierarchy}/{instance_name}") + if cell["type"] in ["$assume", "$assert", "$cover", "$live"]: + try: + location = cell["attributes"]["src"] + except KeyError: + location = "" + p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=f"{hierarchy}/{instance_name}") + mod.properties.append(p) + return mod + + for module_name in design_json["modules"]: + attrs = design_json["modules"][module_name]["attributes"] + if "top" in attrs and int(attrs["top"]) == 1: + hierarchy = make_mod_hier(module_name, module_name) + return hierarchy + else: + raise ValueError("Cannot find top module") + +def main(): + import sys + if len(sys.argv) != 2: + print(f"""Usage: {sys.argv[0]} design.json""") + with open(sys.argv[1]) as f: + print(design_hierarchy(f)) + +if __name__ == '__main__': + main() -- 2.30.2