Merge pull request #133 from nakengelhardt/sby_junit

improve SBY JUnit report

.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

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, platform
 
 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,8 @@ def run_task(taskname):
 
     if not my_opt_tmpdir and not setupmode:
         with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
-            junit_errors = 1 if task.retcode == 16 else 0
+            task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)
-            junit_failures = 1 if task.retcode != 0 and junit_errors == 0 else 0
+
-            print('<?xml version="1.0" encoding="UTF-8"?>', file=f)
-            print(f'<testsuites disabled="0" errors="{junit_errors}" failures="{junit_failures}" tests="1" time="{task.total_time}">', file=f)
-            print(f'<testsuite disabled="0" errors="{junit_errors}" failures="{junit_failures}" name="{junit_ts_name}" skipped="0" tests="1" time="{task.total_time}">', file=f)
-            print('<properties>', file=f)
-            print(f'<property name="os" value="{os.name}"/>', file=f)
-            print('</properties>', file=f)
-            print(f'<testcase classname="{junit_ts_name}" name="{junit_tc_name}" status="{task.status}" time="{task.total_time}">', file=f)
-            if junit_errors:
-                print(f'<error message="{task.status}" type="{task.status}"/>', file=f)
-            if junit_failures:
-                print(f'<failure message="{task.status}" type="{task.status}"/>', file=f)
-            print('<system-out>', end="", file=f)
-            with open(f"{task.workdir}/logfile.txt", "r") as logf:
-                for line in logf:
-                    print(line.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;").replace("\"", "&quot;"), end="", file=f)
-            print('</system-out></testcase></testsuite></testsuites>', file=f)
         with open(f"{task.workdir}/status", "w") as f:
             print(f"{task.status} {task.retcode} {task.total_time}", file=f)
 
@@ -488,7 +472,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)

sbysrc/sby_core.py

@@ -16,13 +16,14 @@
 # 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 = []
 
@@ -221,7 +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 = {
@@ -299,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)
@@ -364,49 +369,64 @@ class SbyTask:
         if not os.path.isdir(f"{self.workdir}/model"):
             os.makedirs(f"{self.workdir}/model")
 
-        if model_name in ["base", "nomem"]:
+        def print_common_prep():
-            with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.ys""", "w") as 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)
+
+        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)
-                if model_name == "base":
+                # the user must designate a top module in [script]
-                    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_json ../model/design.json""", 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"],
+                "cd {}/src; {} -ql ../model/design.log ../model/design.ys".format(self.workdir, self.exe_paths["yosys"])
-                    s="" if model_name == "base" else "_nomem")
             )
             proc.checkretcode = True
 
+            def instance_hierarchy_callback(retcode):
+                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)
+
+            proc.exit_callback = instance_hierarchy_callback
+
             return [proc]
 
         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)
@@ -424,7 +444,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
@@ -434,7 +454,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:
@@ -454,7 +479,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
@@ -464,7 +489,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)
@@ -481,7 +508,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
@@ -721,3 +748,86 @@ 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_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 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
+            junit_failures = 1 if self.retcode != 0 and junit_errors == 0 else 0
+            junit_skipped = 0
+        print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
+        print(f'<testsuites>', file=f)
+        print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="0" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
+        print(f'<properties>', file=f)
+        print(f'<property name="os" value="{platform.system()}"/>', file=f)
+        print(f'<property name="expect" value="{", ".join(self.expect)}"/>', file=f)
+        print(f'<property name="status" value="{self.status}"/>', file=f)
+        print(f'</properties>', file=f)
+        if self.precise_prop_status:
+            print(f'<testcase classname="{junit_tc_name}" name="build execution" time="0">', file=f)
+            if self.retcode == 16:
+                print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
+            elif self.retcode != 0:
+                print(f'<failure type="{junit_type}" message="{self.status}" />', file=f)
+            print(f'</testcase>', file=f)
+
+            for check in checks:
+                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}"'
+                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'<testcase classname="{junit_tc_name}" name="{junit_prop_name}" time="0"{detail_attrs}>', file=f)
+                if check.status == "PASS":
+                    pass
+                elif check.status == "UNKNOWN":
+                    print(f'<skipped />', file=f)
+                elif check.status == "FAIL":
+                    traceinfo = f' Trace file: {check.tracefile}' if check.type == check.Type.ASSERT else ''
+                    print(f'<failure type="{check.type}" message="{junit_prop_name} failed.{traceinfo}" />', file=f)
+                elif check.status == "ERROR":
+                    print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
+                print(f'</testcase>', file=f)
+        else:
+            junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode
+            print(f'<testcase classname="{junit_tc_name}" name="{junit_tc_name}" time="{self.total_time}">', file=f)
+            if junit_errors:
+                print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
+            elif junit_failures:
+                print(f'<failure type="{junit_type}" message="{self.status}" />', file=f)
+            print(f'</testcase>', file=f)
+        print('<system-out>', end="", file=f)
+        with open(f"{self.workdir}/logfile.txt", "r") as logf:
+            for line in logf:
+                print(line.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;").replace("\"", "&quot;"), end="", file=f)
+        print('</system-out>', file=f)
+        print('<system-err>', file=f)
+        #TODO: can we handle errors and still output this file?
+        print('</system-err>', file=f)
+        print(f'</testsuite>', file=f)
+        print(f'</testsuites>', file=f)

sbysrc/sby_design.py

@@ -0,0 +1,139 @@
+#
+# 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 __str__(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="")
+
+    def __repr__(self):
+        return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">"
+
+@dataclass
+class SbyModule:
+    name: str
+    type: str
+    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 __iter__(self):
+        for prop in self.properties:
+            yield prop
+        for submod in self.submodules.values():
+            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
+        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 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=""):
+        # 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():
+            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=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=sub_hierarchy)
+                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:
+        d = design_hierarchy(f)
+        print("Design Hierarchy:", d)
+        for p in d.get_property_list():
+            print("Property:", p)
+
+if __name__ == '__main__':
+    main()

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,34 @@ def run(mode, task, engine_idx, engine):
             proc_status = "ERROR"
             return line
 
+        match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
+        if match:
+            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+) \((\S+)\) in step \d+.", line)
+        if match:
+            cell_name = match[2]
+            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:
+            cell_name = match[2]
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop.status = "FAIL"
+
         return line
 
     def exit_callback(retcode):
@@ -206,6 +237,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()
 
@@ -238,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()

tests/JUnit.xsd

@@ -0,0 +1,232 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<xs:schema
+	xmlns:xs="http://www.w3.org/2001/XMLSchema"
+	 elementFormDefault="qualified"
+	 attributeFormDefault="unqualified">
+	<xs:annotation>
+		<xs:documentation xml:lang="en">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).</xs:documentation>
+	</xs:annotation>
+	<xs:element name="testsuite" type="testsuite"/>
+	<xs:simpleType name="ISO8601_DATETIME_PATTERN">
+		<xs:restriction base="xs:dateTime">
+			<xs:pattern value="[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}"/>
+		</xs:restriction>
+	</xs:simpleType>
+	<xs:element name="testsuites">
+		<xs:annotation>
+			<xs:documentation xml:lang="en">Contains an aggregation of testsuite results</xs:documentation>
+		</xs:annotation>
+		<xs:complexType>
+			<xs:sequence>
+				<xs:element name="testsuite" minOccurs="0" maxOccurs="unbounded">
+					<xs:complexType>
+						<xs:complexContent>
+							<xs:extension base="testsuite">
+								<xs:attribute name="package" type="xs:token" use="required">
+									<xs:annotation>
+										<xs:documentation xml:lang="en">Derived from testsuite/@name in the non-aggregated documents</xs:documentation>
+									</xs:annotation>
+								</xs:attribute>
+								<xs:attribute name="id" type="xs:int" use="required">
+									<xs:annotation>
+										<xs:documentation xml:lang="en">Starts at '0' for the first testsuite and is incremented by 1 for each following testsuite</xs:documentation>
+									</xs:annotation>
+								</xs:attribute>
+							</xs:extension>
+						</xs:complexContent>
+					</xs:complexType>
+				</xs:element>
+			</xs:sequence>
+		</xs:complexType>
+	</xs:element>
+	<xs:complexType name="testsuite">
+		<xs:annotation>
+			<xs:documentation xml:lang="en">Contains the results of exexuting a testsuite</xs:documentation>
+		</xs:annotation>
+		<xs:sequence>
+			<xs:element name="properties">
+				<xs:annotation>
+					<xs:documentation xml:lang="en">Properties (e.g., environment settings) set during test execution</xs:documentation>
+				</xs:annotation>
+				<xs:complexType>
+					<xs:sequence>
+						<xs:element name="property" minOccurs="0" maxOccurs="unbounded">
+							<xs:complexType>
+								<xs:attribute name="name" use="required">
+									<xs:simpleType>
+										<xs:restriction base="xs:token">
+											<xs:minLength value="1"/>
+										</xs:restriction>
+									</xs:simpleType>
+								</xs:attribute>
+								<xs:attribute name="value" type="xs:string" use="required"/>
+							</xs:complexType>
+						</xs:element>
+					</xs:sequence>
+				</xs:complexType>
+			</xs:element>
+			<xs:element name="testcase" minOccurs="0" maxOccurs="unbounded">
+				<xs:complexType>
+					<xs:choice minOccurs="0">
+						<xs:element name="skipped" />
+						<xs:element name="error" minOccurs="0" maxOccurs="1">
+							<xs:annotation>
+								<xs:documentation xml:lang="en">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</xs:documentation>
+							</xs:annotation>
+							<xs:complexType>
+								<xs:simpleContent>
+									<xs:extension base="pre-string">
+										<xs:attribute name="message" type="xs:string">
+											<xs:annotation>
+												<xs:documentation xml:lang="en">The error message. e.g., if a java exception is thrown, the return value of getMessage()</xs:documentation>
+											</xs:annotation>
+										</xs:attribute>
+										<xs:attribute name="type" type="xs:string" use="required">
+											<xs:annotation>
+												<xs:documentation xml:lang="en">The type of error that occured. e.g., if a java execption is thrown the full class name of the exception.</xs:documentation>
+											</xs:annotation>
+										</xs:attribute>
+									</xs:extension>
+								</xs:simpleContent>
+							</xs:complexType>
+						</xs:element>
+						<xs:element name="failure">
+							<xs:annotation>
+								<xs:documentation xml:lang="en">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</xs:documentation>
+							</xs:annotation>
+							<xs:complexType>
+								<xs:simpleContent>
+									<xs:extension base="pre-string">
+										<xs:attribute name="message" type="xs:string">
+											<xs:annotation>
+												<xs:documentation xml:lang="en">The message specified in the assert</xs:documentation>
+											</xs:annotation>
+										</xs:attribute>
+										<xs:attribute name="type" type="xs:string" use="required">
+											<xs:annotation>
+												<xs:documentation xml:lang="en">The type of the assert.</xs:documentation>
+											</xs:annotation>
+										</xs:attribute>
+									</xs:extension>
+								</xs:simpleContent>
+							</xs:complexType>
+						</xs:element>
+					</xs:choice>
+					<xs:attribute name="name" type="xs:token" use="required">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Name of the test method</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="classname" type="xs:token" use="required">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Full class name for the class the test method is in.</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="time" type="xs:decimal" use="required">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Time taken (in seconds) to execute the test</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="id" type="xs:string" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Cell ID of the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="type" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Kind of property (assert, cover, live)</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="location" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Source location of the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+					<xs:attribute name="tracefile" type="xs:token" use="optional">
+						<xs:annotation>
+							<xs:documentation xml:lang="en">Tracefile for the property</xs:documentation>
+						</xs:annotation>
+					</xs:attribute>
+				</xs:complexType>
+			</xs:element>
+			<xs:element name="system-out">
+				<xs:annotation>
+					<xs:documentation xml:lang="en">Data that was written to standard out while the test was executed</xs:documentation>
+				</xs:annotation>
+				<xs:simpleType>
+					<xs:restriction base="pre-string">
+						<xs:whiteSpace value="preserve"/>
+					</xs:restriction>
+				</xs:simpleType>
+			</xs:element>
+			<xs:element name="system-err">
+				<xs:annotation>
+					<xs:documentation xml:lang="en">Data that was written to standard error while the test was executed</xs:documentation>
+				</xs:annotation>
+				<xs:simpleType>
+					<xs:restriction base="pre-string">
+						<xs:whiteSpace value="preserve"/>
+					</xs:restriction>
+				</xs:simpleType>
+			</xs:element>
+		</xs:sequence>
+		<xs:attribute name="name" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">Full class name of the test for non-aggregated testsuite documents. Class name without the package for aggregated testsuites documents</xs:documentation>
+			</xs:annotation>
+			<xs:simpleType>
+				<xs:restriction base="xs:token">
+					<xs:minLength value="1"/>
+				</xs:restriction>
+			</xs:simpleType>
+		</xs:attribute>
+		<xs:attribute name="timestamp" type="ISO8601_DATETIME_PATTERN" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">when the test was executed. Timezone may not be specified.</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+		<xs:attribute name="hostname" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">Host on which the tests were executed. 'localhost' should be used if the hostname cannot be determined.</xs:documentation>
+			</xs:annotation>
+			<xs:simpleType>
+				<xs:restriction base="xs:token">
+					<xs:minLength value="1"/>
+				</xs:restriction>
+			</xs:simpleType>
+		</xs:attribute>
+		<xs:attribute name="tests" type="xs:int" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">The total number of tests in the suite</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+		<xs:attribute name="failures" type="xs:int" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">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</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+		<xs:attribute name="errors" type="xs:int" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">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.</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+		<xs:attribute name="skipped" type="xs:int" use="optional">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">The total number of ignored or skipped tests in the suite.</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+		<xs:attribute name="time" type="xs:decimal" use="required">
+			<xs:annotation>
+				<xs:documentation xml:lang="en">Time taken (in seconds) to execute the tests in the suite</xs:documentation>
+			</xs:annotation>
+		</xs:attribute>
+	</xs:complexType>
+	<xs:simpleType name="pre-string">
+		<xs:restriction base="xs:string">
+			<xs:whiteSpace value="preserve"/>
+		</xs:restriction>
+	</xs:simpleType>
+</xs:schema>

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)
+	python3 validate_junit.py $@/$@.xml

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]

tests/cover_fail.sby

@@ -0,0 +1,31 @@
+[options]
+mode cover
+depth 5
+expect pass,fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read -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 && !rst);
+cover (count == 4'd11 && !rst);
+end
+endmodule

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

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

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

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

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]

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]

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]

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]

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 -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

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()