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/sbysrc/sby.py b/sbysrc/sby.py index 58f02d8..5616bc0 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, 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 - 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) - 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('', 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) + 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) @@ -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) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f05b31d..e1ee51c 100644 --- a/sbysrc/sby_core.py +++ b/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"]: - 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) - 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) + # the user must designate a top module in [script] 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"], - 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): + 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'', 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) + 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 = '' + 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'', 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) + 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) + 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: + 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) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py new file mode 100644 index 0000000..98a57f1 --- /dev/null +++ b/sbysrc/sby_design.py @@ -0,0 +1,139 @@ +# +# 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 __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() diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index da2e31c..492e2a5 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,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() diff --git a/tests/JUnit.xsd b/tests/JUnit.xsd new file mode 100644 index 0000000..7a5f184 --- /dev/null +++ b/tests/JUnit.xsd @@ -0,0 +1,232 @@ + + + + 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 + + + + + Cell ID of the property + + + + + Kind of property (assert, cover, live) + + + + + Source location of the property + + + + + Tracefile for the property + + + + + + + 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/Makefile b/tests/Makefile index 58971e6..9370991 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) + python3 validate_junit.py $@/$@.xml 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 new file mode 100644 index 0000000..391e0a8 --- /dev/null +++ b/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 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_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 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 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 new file mode 100644 index 0000000..93abc9c --- /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 -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 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()