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):
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:
junit_time = time.strftime('%Y-%m-%dT%H:%M:%S')
print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
print(f'<testsuites>', file=f)
- #TODO: check with Micko if os.uname().nodename is sane enough in most places
- print(f'<testsuite timestamp="{junit_time}" hostname="{os.uname().nodename}" package="" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{task.total_time}" skipped="{junit_tests - junit_failures}">', file=f)
+ print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{task.total_time}" skipped="{junit_tests - junit_failures}">', file=f)
print(f'<properties>', file=f)
- print(f'<property name="os" value="{os.name}"/>', file=f)
+ print(f'<property name="os" value="{platform.system()}"/>', file=f)
print(f'</properties>', file=f)
- if solver_gives_line:
+ if task.precise_prop_status:
for check in checks:
- print(f'<testcase classname="{junit_tc_name}" name="Property {check.type} in {check.hierarchy} at {check.location}" time="{task.total_time}">', file=f) # name required
- if check.status == "UNKNOWN":
+ detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"'
+ print(f'<testcase classname="{junit_tc_name}" name="Property {check.type} in {check.hierarchy} at {check.location}" time="{task.total_time}"{detail_attrs}>', file=f) # name required
+ if check.status == "PASS":
+ pass
+ elif 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)
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
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=""):
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()
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)
)
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:
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()
projects / SymbiYosys.git / commitdiff