From cdf5650c12dc4bfc4036b5fdb7456610959358ce Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 7 Dec 2021 20:14:06 +0100 Subject: [PATCH 01/14] add JUnit schema and validator Signed-off-by: N. Engelhardt --- tests/JUnit.xsd | 212 ++++++++++++++++++++++++++++++++++++++++ tests/validate_junit.py | 19 ++++ 2 files changed, 231 insertions(+) create mode 100644 tests/JUnit.xsd create mode 100644 tests/validate_junit.py diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd new file mode 100644 index 0000000..84b0f15 --- /dev/null +++ b/tests/JUnit.xsd @@ -0,0 +1,212 @@ + + + + JUnit test result schema for the Apache Ant JUnit and JUnitReport tasks +Copyright © 2011, Windy Road Technology Pty. Limited +The Apache Ant JUnit XML Schema is distributed under the terms of the Apache License Version 2.0 http://www.apache.org/licenses/ +Permission to waive conditions of this license may be requested from Windy Road Support (http://windyroad.org/support). + + + + + + + + + + Contains an aggregation of testsuite results + + + + + + + + + + Derived from testsuite/@name in the non-aggregated documents + + + + + Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite + + + + + + + + + + + + Contains the results of exexuting a testsuite + + + + + Properties (e.g., environment settings) set during test execution + + + + + + + + + + + + + + + + + + + + + + + + + Indicates that the test errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. Contains as a text node relevant data for the error, e.g., a stack trace + + + + + + + The error message. e.g., if a java exception is thrown, the return value of getMessage() + + + + + The type of error that occured. e.g., if a java execption is thrown the full class name of the exception. + + + + + + + + + Indicates that the test failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals. Contains as a text node relevant data for the failure, e.g., a stack trace + + + + + + + The message specified in the assert + + + + + The type of the assert. + + + + + + + + + + Name of the test method + + + + + Full class name for the class the test method is in. + + + + + Time taken (in seconds) to execute the test + + + + + + + Data that was written to standard out while the test was executed + + + + + + + + + + Data that was written to standard error while the test was executed + + + + + + + + + + + Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents + + + + + + + + + + when the test was executed. Timezone may not be specified. + + + + + Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined. + + + + + + + + + + The total number of tests in the suite + + + + + The total number of tests in the suite that failed. A failure is a test which the code has explicitly failed by using the mechanisms for that purpose. e.g., via an assertEquals + + + + + The total number of tests in the suite that errored. An errored test is one that had an unanticipated problem. e.g., an unchecked throwable; or a problem with the implementation of the test. + + + + + The total number of ignored or skipped tests in the suite. + + + + + Time taken (in seconds) to execute the tests in the suite + + + + + + + + + diff --git a/tests/validate_junit.py b/tests/validate_junit.py new file mode 100644 index 0000000..c1c0573 --- /dev/null +++ b/tests/validate_junit.py @@ -0,0 +1,19 @@ +from xmlschema import XMLSchema, XMLSchemaValidationError +import argparse + +def main(): + parser = argparse.ArgumentParser(description="Validate JUnit output") + parser.add_argument('xml') + parser.add_argument('--xsd', default="JUnit.xsd") + + args = parser.parse_args() + + schema = XMLSchema(args.xsd) + try: + schema.validate(args.xml) + except XMLSchemaValidationError as e: + print(e) + exit(1) + +if __name__ == '__main__': + main() From 6ec2df34e36c69916a5da2f67c464eff85624590 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 7 Dec 2021 20:16:15 +0100 Subject: [PATCH 02/14] WIP change junit print to conform to schema; needs additional data, currently printing dummy info Signed-off-by: N. Engelhardt --- sbysrc/sby.py | 51 +++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 37 insertions(+), 14 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 58f02d8..c720b22 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 -from time import localtime +import time class DictAction(argparse.Action): def __call__(self, parser, namespace, values, option_string=None): @@ -156,7 +156,7 @@ prep -top top early_logmsgs = list() def early_log(workdir, msg): - tm = localtime() + tm = time.localtime() early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg)) print(early_logmsgs[-1]) @@ -455,24 +455,47 @@ 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'} + ] + 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 - print('', file=f) - print(f'', file=f) - print(f'', file=f) - print('', file=f) + 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) + 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('', file=f) - print(f'', file=f) - if junit_errors: - print(f'', file=f) - if junit_failures: - print(f'', file=f) + print(f'', file=f) + for check in checks: + print(f'', file=f) # name required + 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 + print(f'', file=f) print('', end="", file=f) with open(f"{task.workdir}/logfile.txt", "r") as logf: for line in logf: print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) - print('', file=f) + print('', file=f) + print('', file=f) + #TODO: can we handle errors and still output this file? + print('', file=f) + print(f'', file=f) + print(f'', file=f) + with open(f"{task.workdir}/status", "w") as f: print(f"{task.status} {task.retcode} {task.total_time}", file=f) @@ -488,7 +511,7 @@ for task in tasknames: failed.append(task) if failed and (len(tasknames) > 1 or tasknames[0] is not None): - tm = localtime() + tm = time.localtime() print("SBY {:2d}:{:02d}:{:02d} The following tasks failed: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, failed)) sys.exit(retcode) From 7f3c4137c10c79c671a8f20b8d6b20a16487beee Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 19 Jan 2022 19:34:11 +0100 Subject: [PATCH 03/14] 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() From a9d1972c47a158fc139847b7661592e1a25300cb Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Fri, 21 Jan 2022 15:18:53 +0100 Subject: [PATCH 04/14] add fallback if solver can't tell which property fails --- sbysrc/sby.py | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 3d2f583..f3b78ea 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -458,11 +458,15 @@ 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 task.retcode != 0 and junit_errors == 0: - for check in checks: - if check.status == "FAIL": - junit_failures += 1 + if junit_errors == 0 and task.retcode != 0: + if solver_gives_line: + for check in checks: + if check.status == "FAIL": + junit_failures += 1 + else: + 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) @@ -472,13 +476,23 @@ def run_task(taskname): print(f'', file=f) print(f'', file=f) print(f'', file=f) - for check in checks: + if solver_gives_line: + for check in checks: + print(f'', file=f) # name required + 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 + print(f'', file=f) + else: print(f'', file=f) # name required - if check.status == "UNKNOWN": + if task.status == "UNKNOWN": print(f'', file=f) - elif check.status == "FAIL": - print(f'', file=f) - elif check.status == "ERROR": + elif task.status == "FAIL": + print(f'', file=f) + elif task.status == "ERROR": print(f'', file=f) # type mandatory, message optional print(f'', file=f) print('', end="", file=f) From 1cf27e7c315daa6019a9a6398a9827cfddf9c84b Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 27 Jan 2022 13:41:07 +0100 Subject: [PATCH 05/14] 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 From d7e7f2c530cd88b05793af8a15d615a8b61a860b Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 31 Jan 2022 12:35:56 +0100 Subject: [PATCH 06/14] refactor model to have single base --- sbysrc/sby_core.py | 77 ++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 34 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ec4e0a1..dde634b 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -367,50 +367,47 @@ class SbyTask: if not os.path.isdir(f"{self.workdir}/model"): os.makedirs(f"{self.workdir}/model") - if model_name in ["base", "nomem"]: - with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.ys""", "w") as f: + def print_common_prep(): + if self.opt_multiclock: + print("clk2fflogic", file=f) + else: + print("async2sync", file=f) + print("chformal -assume -early", file=f) + if self.opt_mode in ["bmc", "prove"]: + print("chformal -live -fair -cover -remove", file=f) + if self.opt_mode == "cover": + print("chformal -live -fair -remove", file=f) + if self.opt_mode == "live": + print("chformal -assert2assume", file=f) + print("chformal -cover -remove", file=f) + print("opt_clean", file=f) + print("setundef -anyseq", file=f) + print("opt -keepdc -fast", file=f) + print("check", file=f) + print("hierarchy -simcheck", file=f) + + if model_name == "base": + with open(f"""{self.workdir}/model/design.ys""", "w") as f: 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 + # the user must designate a top module in [script] print("hierarchy -simcheck", file=f) print(f"""write_json ../model/design.json""", file=f) - if model_name == "base": - print("memory_nordff", file=f) - else: - print("memory_map", file=f) - if self.opt_multiclock: - print("clk2fflogic", file=f) - else: - print("async2sync", file=f) - print("chformal -assume -early", file=f) - if self.opt_mode in ["bmc", "prove"]: - print("chformal -live -fair -cover -remove", file=f) - if self.opt_mode == "cover": - print("chformal -live -fair -remove", file=f) - if self.opt_mode == "live": - print("chformal -assert2assume", file=f) - print("chformal -cover -remove", file=f) - print("opt_clean", file=f) - print("setundef -anyseq", file=f) - print("opt -keepdc -fast", file=f) - print("check", file=f) - print("hierarchy -simcheck", file=f) - print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f) + print(f"""write_rtlil ../model/design.il""", file=f) proc = SbyProc( self, model_name, [], - "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"], - s="" if model_name == "base" else "_nomem") + "cd {}/src; {} -ql ../model/design.log ../model/design.ys".format(self.workdir, self.exe_paths["yosys"]) ) proc.checkretcode = True def instance_hierarchy_callback(retcode): assert retcode == 0 if self.design_hierarchy == None: - with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f: + with open(f"{self.workdir}/model/design.json") as f: self.design_hierarchy = design_hierarchy(f) proc.exit_callback = instance_hierarchy_callback @@ -420,7 +417,12 @@ class SbyTask: if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name): with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f: print(f"# running in {self.workdir}/model/", file=f) - print(f"""read_ilang design{"_nomem" if "_nomem" in model_name else ""}.il""", file=f) + print(f"""read_ilang design.il""", file=f) + if "_nomem" in model_name: + print("memory_map", file=f) + else: + print("memory_nordff", file=f) + print_common_prep() if "_syn" in model_name: print("techmap", file=f) print("opt -fast", file=f) @@ -438,7 +440,7 @@ class SbyTask: proc = SbyProc( self, model_name, - self.model("nomem" if "_nomem" in model_name else "base"), + self.model("base"), "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name) ) proc.checkretcode = True @@ -448,7 +450,12 @@ class SbyTask: if re.match(r"^btor(_syn)?(_nomem)?$", model_name): with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f: print(f"# running in {self.workdir}/model/", file=f) - print(f"""read_ilang design{"_nomem" if "_nomem" in model_name else ""}.il""", file=f) + print(f"""read_ilang design.il""", file=f) + if "_nomem" in model_name: + print("memory_map", file=f) + else: + print("memory_nordff", file=f) + print_common_prep() print("flatten", file=f) print("setundef -undriven -anyseq", file=f) if "_syn" in model_name: @@ -468,7 +475,7 @@ class SbyTask: proc = SbyProc( self, model_name, - self.model("nomem" if "_nomem" in model_name else "base"), + self.model("base"), "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name) ) proc.checkretcode = True @@ -478,7 +485,9 @@ class SbyTask: if model_name == "aig": with open(f"{self.workdir}/model/design_aiger.ys", "w") as f: print(f"# running in {self.workdir}/model/", file=f) - print("read_ilang design_nomem.il", file=f) + print("read_ilang design.il", file=f) + print("memory_map", file=f) + print_common_prep() print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f) @@ -495,7 +504,7 @@ class SbyTask: proc = SbyProc( self, "aig", - self.model("nomem"), + self.model("base"), f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_aiger.log design_aiger.ys""" ) proc.checkretcode = True From 9168b0163bfe3e9bffca915bdae05d27ffc5f992 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Sun, 6 Feb 2022 09:15:44 +0100 Subject: [PATCH 07/14] 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() From 5abaccab695063a65fe54748b8e7dcc02428838d Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 7 Feb 2022 12:29:27 +0100 Subject: [PATCH 08/14] refactor junit print into own function --- sbysrc/sby.py | 52 +-------------------------------------- sbysrc/sby_core.py | 61 ++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 60 insertions(+), 53 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index ee8f1a3..788c68b 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -455,57 +455,7 @@ def run_task(taskname): if not my_opt_tmpdir and not setupmode: with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f: - checks = task.design_hierarchy.get_property_list() - junit_tests = len(checks) - junit_errors = 1 if task.retcode == 16 else 0 - junit_failures = 0 - if junit_errors == 0 and task.retcode != 0: - if solver_gives_line: - for check in checks: - if check.status == "FAIL": - junit_failures += 1 - else: - 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) - print(f'', file=f) - print(f'', file=f) - print(f'', file=f) - print(f'', file=f) - print(f'', file=f) - if task.precise_prop_status: - for check in checks: - 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) - elif check.status == "ERROR": - print(f'', file=f) # type mandatory, message optional - print(f'', file=f) - else: - print(f'', file=f) # name required - if task.status == "UNKNOWN": - print(f'', file=f) - elif task.status == "FAIL": - print(f'', file=f) - elif task.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: - for line in logf: - print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) - print('', file=f) - print('', file=f) - #TODO: can we handle errors and still output this file? - print('', file=f) - print(f'', file=f) - print(f'', file=f) + task.print_junit_result(f, junit_ts_name, junit_tc_name) with open(f"{task.workdir}/status", "w") as f: print(f"{task.status} {task.retcode} {task.total_time}", file=f) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index dde634b..9c7e3fd 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -16,13 +16,13 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import os, re, sys, signal +import os, re, sys, signal, platform if os.name == "posix": import resource, fcntl import subprocess from shutil import copyfile, copytree, rmtree from select import select -from time import time, localtime, sleep +from time import time, localtime, sleep, strftime from sby_design import SbyProperty, SbyModule, design_hierarchy all_procs_running = [] @@ -744,3 +744,60 @@ class SbyTask: with open(f"{self.workdir}/{self.status}", "w") as f: for line in self.summary: print(line, file=f) + + def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False): + junit_errors = 1 if self.retcode == 16 else 0 + if self.precise_prop_status: + checks = self.design_hierarchy.get_property_list() + junit_tests = len(checks) + else: + junit_tests = 1 + if self.retcode in [0, 16]: + junit_failures = 0 + else: + if self.precise_prop_status: + for check in checks: + if check.status not in self.expect: + junit_failures += 1 + else: + junit_failures = 1 + junit_time = strftime('%Y-%m-%dT%H:%M:%S') + 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 self.precise_prop_status: + for check in checks: + detail_attrs = '' if junit_format_strict else 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) + elif check.status == "ERROR": + print(f'', file=f) # type mandatory, message optional + print(f'', file=f) + else: + junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode + print(f'', file=f) # name required + if self.status == "UNKNOWN": + print(f'', file=f) + elif self.status == "FAIL": + print(f'', file=f) + elif self.status == "ERROR": + print(f'', file=f) # type mandatory, message optional + print(f'', file=f) + print('', end="", file=f) + with open(f"{self.workdir}/logfile.txt", "r") as logf: + for line in logf: + print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) + print('', file=f) + print('', file=f) + #TODO: can we handle errors and still output this file? + print('', file=f) + print(f'', file=f) + print(f'', file=f) From 53eb25fcaeddfdb7011ddba98c67f85b903fe8f0 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 7 Feb 2022 15:29:36 +0100 Subject: [PATCH 09/14] handle unreached cover properties --- sbysrc/sby.py | 2 +- sbysrc/sby_core.py | 4 +++- sbysrc/sby_engine_smtbmc.py | 6 ++++++ tests/cover_fail.sby | 31 +++++++++++++++++++++++++++++++ 4 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 tests/cover_fail.sby diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 788c68b..5616bc0 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -455,7 +455,7 @@ def run_task(taskname): if not my_opt_tmpdir and not setupmode: with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f: - task.print_junit_result(f, junit_ts_name, junit_tc_name) + task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False) with open(f"{task.workdir}/status", "w") as f: print(f"{task.status} {task.retcode} {task.total_time}", file=f) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 9c7e3fd..8668b9d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -756,6 +756,7 @@ class SbyTask: junit_failures = 0 else: if self.precise_prop_status: + junit_failures = 0 for check in checks: if check.status not in self.expect: junit_failures += 1 @@ -777,7 +778,8 @@ class SbyTask: elif check.status == "UNKNOWN": print(f'', file=f) elif check.status == "FAIL": - print(f'', file=f) + traceinfo = f' Trace file: {check.tracefile}' if check.type == check.Type.ASSERT else '' + print(f'', file=f) elif check.status == "ERROR": print(f'', file=f) # type mandatory, message optional print(f'', file=f) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index e179dd5..a2553f2 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -201,6 +201,12 @@ def run(mode, task, engine_idx, engine): last_prop.tracefile = match[1] last_prop = None + match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line) + if match: + cell_name = match[2] + prop = task.design_hierarchy.find_property_by_cellname(cell_name) + prop.status = "FAIL" + return line def exit_callback(retcode): diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby new file mode 100644 index 0000000..f169a5f --- /dev/null +++ b/tests/cover_fail.sby @@ -0,0 +1,31 @@ +[options] +mode cover +depth 5 +expect fail + +[engines] +smtbmc boolector + +[script] +read_verilog -sv test.v +prep -top test + +[file test.v] +module test( +input clk, +input rst, +output reg [3:0] count +); + +initial assume (rst == 1'b1); + +always @(posedge clk) begin +if (rst) + count <= 4'b0; +else + count <= count + 1'b1; + +cover (count == 0); +cover (count == 4'd11); +end +endmodule From 7d3545dc86c9c6f33f87d9fad18d388e76ef526e Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 7 Feb 2022 19:20:29 +0100 Subject: [PATCH 10/14] fix junit error/failure/skipped count --- sbysrc/sby_core.py | 53 ++++++++++++++++++++++--------------- sbysrc/sby_engine_smtbmc.py | 4 ++- tests/cover_fail.sby | 4 +-- 3 files changed, 37 insertions(+), 24 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 8668b9d..7535d71 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -302,6 +302,8 @@ class SbyTask: self.status = "ERROR" if "ERROR" not in self.expect: self.retcode = 16 + else: + self.retcode = 0 self.terminate() with open(f"{self.workdir}/{self.status}", "w") as f: print(f"ERROR: {logmessage}", file=f) @@ -746,33 +748,44 @@ class SbyTask: print(line, file=f) def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False): - junit_errors = 1 if self.retcode == 16 else 0 + junit_time = strftime('%Y-%m-%dT%H:%M:%S') if self.precise_prop_status: checks = self.design_hierarchy.get_property_list() junit_tests = len(checks) + junit_failures = 0 + junit_errors = 0 + junit_skipped = 0 + for check in checks: + if check.status == "PASS": + pass + elif check.status == "FAIL": + junit_failures += 1 + elif check.status == "UNKNOWN": + junit_skipped += 1 + else: + junit_errors += 1 + if junit_errors == 0 and self.status == "ERROR": + junit_errors = 1 else: junit_tests = 1 - if self.retcode in [0, 16]: - junit_failures = 0 - else: - if self.precise_prop_status: - junit_failures = 0 - for check in checks: - if check.status not in self.expect: - junit_failures += 1 - else: - junit_failures = 1 - junit_time = strftime('%Y-%m-%dT%H:%M:%S') + junit_errors = 1 if self.retcode == 16 else 0 + junit_failures = 1 if self.retcode != 0 and junit_errors == 0 else 0 + junit_skipped = 0 print(f'', file=f) 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 self.precise_prop_status: for check in checks: - detail_attrs = '' if junit_format_strict else f' type="{check.type}" location="{check.location}" id="{check.name}"' - print(f'', file=f) # name required + if junit_format_strict: + detail_attrs = '' + else: + detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"' + if check.tracefile: + detail_attrs += f' tracefile="{check.tracefile}"' + print(f'', file=f) if check.status == "PASS": pass elif check.status == "UNKNOWN": @@ -785,13 +798,11 @@ class SbyTask: print(f'', file=f) else: junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode - print(f'', file=f) # name required - if self.status == "UNKNOWN": - print(f'', file=f) - elif self.status == "FAIL": - print(f'', file=f) - elif self.status == "ERROR": + print(f'', file=f) + if junit_errors: print(f'', file=f) # type mandatory, message optional + elif junit_failures: + print(f'', file=f) print(f'', file=f) print('', end="", file=f) with open(f"{self.workdir}/logfile.txt", "r") as logf: diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index a2553f2..0bf887d 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} --cellinfo --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} --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) ) @@ -195,11 +195,13 @@ def run(mode, task, engine_idx, engine): prop = task.design_hierarchy.find_property_by_cellname(cell_name) prop.status = "PASS" last_prop = prop + return line 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 match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line) if match: diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby index f169a5f..f75a911 100644 --- a/tests/cover_fail.sby +++ b/tests/cover_fail.sby @@ -25,7 +25,7 @@ if (rst) else count <= count + 1'b1; -cover (count == 0); -cover (count == 4'd11); +cover (count == 0 && !rst); +cover (count == 4'd11 && !rst); end endmodule From 7ee357fcc8aa13b7015049f1c89380c5cc074107 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 7 Feb 2022 22:01:52 +0100 Subject: [PATCH 11/14] fix induction --- sbysrc/sby_core.py | 2 +- sbysrc/sby_design.py | 7 ++++--- sbysrc/sby_engine_smtbmc.py | 3 +++ tests/both_ex.sby | 2 +- tests/cover_fail.sby | 2 +- tests/multi_assert.sby | 2 +- tests/preunsat.sby | 2 +- tests/redxor.sby | 2 +- tests/stopfirst.sby | 2 +- tests/submod_props.sby | 2 +- 10 files changed, 15 insertions(+), 11 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 7535d71..ede1a8d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -773,7 +773,7 @@ class SbyTask: junit_skipped = 0 print(f'', file=f) print(f'', file=f) - print(f'', file=f) + print(f'', file=f) print(f'', file=f) print(f'', file=f) print(f'', file=f) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index c0fdb8b..98a57f1 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -51,7 +51,7 @@ class SbyProperty: tracefile: str = field(default="") def __repr__(self): - return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\"" + return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">" @dataclass class SbyModule: @@ -105,14 +105,15 @@ def design_hierarchy(filename): cells = design_json["modules"][module_name]["cells"] for cell_name, cell in cells.items(): + sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name if cell["type"][0] != '$': - mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=f"{hierarchy}/{instance_name}") + mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=sub_hierarchy) 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}") + p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=sub_hierarchy) mod.properties.append(p) return mod diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 0bf887d..492e2a5 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -273,6 +273,9 @@ def run(mode, task, engine_idx, engine): assert False if task.basecase_pass and task.induction_pass: + for prop in task.design_hierarchy: + if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": + prop.status = "PASS" task.update_status("PASS") task.summary.append("successful proof by k-induction.") task.terminate() diff --git a/tests/both_ex.sby b/tests/both_ex.sby index f83f2b1..8177374 100644 --- a/tests/both_ex.sby +++ b/tests/both_ex.sby @@ -15,7 +15,7 @@ pono: btor pono cover: btor btormc [script] -read_verilog -sv both_ex.v +read -sv both_ex.v prep -top test [files] diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby index f75a911..8031e20 100644 --- a/tests/cover_fail.sby +++ b/tests/cover_fail.sby @@ -7,7 +7,7 @@ expect fail smtbmc boolector [script] -read_verilog -sv test.v +read -sv test.v prep -top test [file test.v] diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby index 818195f..883181a 100644 --- a/tests/multi_assert.sby +++ b/tests/multi_assert.sby @@ -12,7 +12,7 @@ btormc: btor btormc pono: btor pono [script] -read_verilog -sv multi_assert.v +read -sv multi_assert.v prep -top test [file multi_assert.v] diff --git a/tests/preunsat.sby b/tests/preunsat.sby index 6694a6c..98255c6 100644 --- a/tests/preunsat.sby +++ b/tests/preunsat.sby @@ -12,7 +12,7 @@ btormc: btor btormc yices: smtbmc yices [script] -read_verilog -sv test.sv +read -sv test.sv prep -top test [file test.sv] diff --git a/tests/redxor.sby b/tests/redxor.sby index 6e6e9f8..0746861 100644 --- a/tests/redxor.sby +++ b/tests/redxor.sby @@ -6,7 +6,7 @@ expect pass btor btormc [script] -read_verilog -formal redxor.v +read -formal redxor.v prep -top test [files] diff --git a/tests/stopfirst.sby b/tests/stopfirst.sby index 35ed539..782f791 100644 --- a/tests/stopfirst.sby +++ b/tests/stopfirst.sby @@ -6,7 +6,7 @@ expect fail btor btormc [script] -read_verilog -sv test.sv +read -sv test.sv prep -top test [file test.sv] diff --git a/tests/submod_props.sby b/tests/submod_props.sby index 33a3a00..93abc9c 100644 --- a/tests/submod_props.sby +++ b/tests/submod_props.sby @@ -12,7 +12,7 @@ expect fail smtbmc boolector [script] -read_verilog -sv test.sv +read -sv test.sv prep -top top [file test.sv] From 89ed843ff1862b740edc812b6b1d245dbccf0721 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 22 Feb 2022 16:16:37 +0100 Subject: [PATCH 12/14] validate junit files (with extra attributes added to schema) --- sbysrc/sby_core.py | 6 ++++- tests/JUnit.xsd | 20 ++++++++++++++++ tests/Makefile | 10 ++++++-- tests/cover_fail.sby | 2 +- tests/junit_assert.sby | 38 +++++++++++++++++++++++++++++++ tests/junit_cover.sby | 43 +++++++++++++++++++++++++++++++++++ tests/junit_timeout_error.sby | 42 ++++++++++++++++++++++++++++++++++ 7 files changed, 157 insertions(+), 4 deletions(-) create mode 100644 tests/junit_assert.sby create mode 100644 tests/junit_cover.sby create mode 100644 tests/junit_timeout_error.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ede1a8d..b50ca3e 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -407,7 +407,9 @@ class SbyTask: proc.checkretcode = True def instance_hierarchy_callback(retcode): - assert retcode == 0 + if retcode != 0: + self.precise_prop_status = False + return if self.design_hierarchy == None: with open(f"{self.workdir}/model/design.json") as f: self.design_hierarchy = design_hierarchy(f) @@ -776,6 +778,8 @@ class SbyTask: 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 self.precise_prop_status: for check in checks: diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd index 84b0f15..7a5f184 100644 --- a/tests/JUnit.xsd +++ b/tests/JUnit.xsd @@ -130,6 +130,26 @@ Permission to waive conditions of this license may be requested from Windy Road Time taken (in seconds) to execute the test + + + Cell ID of the property + + + + + Kind of property (assert, cover, live) + + + + + Source location of the property + + + + + Tracefile for the property + + diff --git a/tests/Makefile b/tests/Makefile index 58971e6..4b8ac35 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,11 +1,17 @@ SBY_FILES=$(wildcard *.sby) SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=)) +JUNIT_TESTS=junit_assert_pass junit_assert_fail junit_assert_preunsat \ +junit_cover_pass junit_cover_uncovered junit_cover_assert junit_cover_preunsat \ +junit_timeout_error_timeout junit_timeout_error_syntax junit_timeout_error_solver -.PHONY: test +.PHONY: test validate_junit FORCE: -test: $(SBY_TESTS) +test: $(JUNIT_TESTS) test_%: %.sby FORCE python3 ../sbysrc/sby.py -f $< + +$(JUNIT_TESTS): $(SBY_TESTS) + python validate_junit.py $@/$@.xml diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby index 8031e20..391e0a8 100644 --- a/tests/cover_fail.sby +++ b/tests/cover_fail.sby @@ -1,7 +1,7 @@ [options] mode cover depth 5 -expect fail +expect pass,fail [engines] smtbmc boolector diff --git a/tests/junit_assert.sby b/tests/junit_assert.sby new file mode 100644 index 0000000..e13f375 --- /dev/null +++ b/tests/junit_assert.sby @@ -0,0 +1,38 @@ +[tasks] +pass +fail +preunsat + +[options] +mode bmc +depth 1 + +pass: expect pass +fail: expect fail +preunsat: expect error + +[engines] +smtbmc boolector + +[script] +fail: read -define FAIL +preunsat: read -define PREUNSAT +read -sv test.sv +prep -top top + +[file test.sv] +module test(input foo); +always @* assert(foo); +`ifdef FAIL +always @* assert(!foo); +`endif +`ifdef PREUNSAT +always @* assume(!foo); +`endif +endmodule + +module top(); +test test_i ( +.foo(1'b1) +); +endmodule diff --git a/tests/junit_cover.sby b/tests/junit_cover.sby new file mode 100644 index 0000000..53747ba --- /dev/null +++ b/tests/junit_cover.sby @@ -0,0 +1,43 @@ +[tasks] +pass +uncovered fail +assert fail +preunsat + +[options] +mode cover +depth 1 + +pass: expect pass +fail: expect fail +preunsat: expect fail + +[engines] +smtbmc boolector + +[script] +uncovered: read -define FAIL +assert: read -define FAIL_ASSERT +preunsat: read -define PREUNSAT +read -sv test.sv +prep -top top + +[file test.sv] +module test(input foo); +`ifdef PREUNSAT +always @* assume(!foo); +`endif +always @* cover(foo); +`ifdef FAIL +always @* cover(!foo); +`endif +`ifdef FAIL_ASSERT +always @* assert(!foo); +`endif +endmodule + +module top(); +test test_i ( +.foo(1'b1) +); +endmodule diff --git a/tests/junit_timeout_error.sby b/tests/junit_timeout_error.sby new file mode 100644 index 0000000..551de49 --- /dev/null +++ b/tests/junit_timeout_error.sby @@ -0,0 +1,42 @@ +[tasks] +syntax error +solver error +timeout + +[options] +mode cover +depth 1 +timeout: timeout 1 +error: expect error +timeout: expect timeout + +[engines] +~solver: smtbmc --dumpsmt2 --progress --stbv z3 +solver: smtbmc foo + +[script] +read -noverific +syntax: read -define SYNTAX_ERROR +read -sv primes.sv +prep -top primes + +[file primes.sv] +module primes; + parameter [8:0] offset = 7; + (* anyconst *) reg [8:0] prime1; + wire [9:0] prime2 = prime1 + offset; + (* allconst *) reg [4:0] factor; + +`ifdef SYNTAX_ERROR + foo +`endif + + always @* begin + if (1 < factor && factor < prime1) + assume ((prime1 % factor) != 0); + if (1 < factor && factor < prime2) + assume ((prime2 % factor) != 0); + assume (1 < prime1); + cover (1); + end +endmodule From 7142f790e4ff6ca6f64e711d6722254643d32ccc Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 24 Feb 2022 22:44:11 +0100 Subject: [PATCH 13/14] add testcase for overall run result --- sbysrc/sby_core.py | 21 +++++++++++++++++---- tests/junit_nocodeloc.sby | 20 ++++++++++++++++++++ 2 files changed, 37 insertions(+), 4 deletions(-) create mode 100644 tests/junit_nocodeloc.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index b50ca3e..e1ee51c 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -766,8 +766,10 @@ class SbyTask: junit_skipped += 1 else: junit_errors += 1 - if junit_errors == 0 and self.status == "ERROR": - junit_errors = 1 + if self.retcode == 16: + junit_errors += 1 + elif self.retcode != 0: + junit_failures += 1 else: junit_tests = 1 junit_errors = 1 if self.retcode == 16 else 0 @@ -782,6 +784,13 @@ class SbyTask: print(f'', file=f) print(f'', file=f) if self.precise_prop_status: + print(f'', file=f) + if self.retcode == 16: + print(f'', file=f) # type mandatory, message optional + elif self.retcode != 0: + print(f'', file=f) + print(f'', file=f) + for check in checks: if junit_format_strict: detail_attrs = '' @@ -789,14 +798,18 @@ class SbyTask: detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"' if check.tracefile: detail_attrs += f' tracefile="{check.tracefile}"' - print(f'', file=f) + if check.location: + junit_prop_name = f"Property {check.type} in {check.hierarchy} at {check.location}" + else: + junit_prop_name = f"Property {check.type} {check.name} in {check.hierarchy}" + print(f'', file=f) if check.status == "PASS": pass elif check.status == "UNKNOWN": print(f'', file=f) elif check.status == "FAIL": traceinfo = f' Trace file: {check.tracefile}' if check.type == check.Type.ASSERT else '' - print(f'', file=f) + print(f'', file=f) elif check.status == "ERROR": print(f'', file=f) # type mandatory, message optional print(f'', file=f) diff --git a/tests/junit_nocodeloc.sby b/tests/junit_nocodeloc.sby new file mode 100644 index 0000000..5d2afc8 --- /dev/null +++ b/tests/junit_nocodeloc.sby @@ -0,0 +1,20 @@ +[options] +mode bmc + +expect fail + +[engines] +smtbmc boolector + +[script] +read -sv multi_assert.v +prep -top test +setattr -unset src + +[file multi_assert.v] +module test(); +always @* begin +assert (1); +assert (0); +end +endmodule From 8a81b61321413f0c47e8ab950b8d36f36976bf2e Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 7 Mar 2022 08:34:01 +0100 Subject: [PATCH 14/14] fix ci --- .github/workflows/ci.yml | 2 +- tests/Makefile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9e05525..ea48d06 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,4 +9,4 @@ jobs: - uses: actions/checkout@v2 - uses: YosysHQ/setup-oss-cad-suite@v1 - name: Run checks - run: make ci + run: tabbypip install xmlschema && make ci diff --git a/tests/Makefile b/tests/Makefile index 4b8ac35..9370991 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -14,4 +14,4 @@ test_%: %.sby FORCE python3 ../sbysrc/sby.py -f $< $(JUNIT_TESTS): $(SBY_TESTS) - python validate_junit.py $@/$@.xml + python3 validate_junit.py $@/$@.xml