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'<?xml version="1.0" encoding="UTF-8"?>', file=f)
print(f'</properties>', file=f)
for check in checks:
print(f'<testcase classname="{junit_tc_name}" name="" time="{task.total_time}">', file=f) # name required
- if check["status"] == "unknown":
+ if check.status == "UNKNOWN":
print(f'<skipped />', file=f)
- elif check["status"] == "fail":
- print(f'<failure type="{check["type"]}" message="Property in {check["hierarchy"]} at {check["location"]} failed. Trace file: {check["tracefile"]}" />', file=f)
- elif check["status"] == "error":
- print(f'<error type="error"/>', file=f) # type mandatory, message optional
+ elif check.status == "FAIL":
+ print(f'<failure type="{check.type}" message="Property in {check.hierarchy} at {check.location} failed. Trace file: {check.tracefile}" />', file=f)
+ elif check.status == "ERROR":
+ print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
print(f'</testcase>', file=f)
print('<system-out>', end="", file=f)
with open(f"{task.workdir}/logfile.txt", "r") as logf:
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 = []
self.status = "UNKNOWN"
self.total_time = 0
self.expect = []
+ self.design_hierarchy = None
yosys_program_prefix = "" ##yosys-program-prefix##
self.exe_paths = {
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(
)
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):
--- /dev/null
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2022 N. Engelhardt <nak@yosyshq.com>
+#
+# 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()
projects / SymbiYosys.git / commitdiff